MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  undifixp Structured version   Visualization version   GIF version

Theorem undifixp 8098
Description: Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.)
Assertion
Ref Expression
undifixp ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ X𝑥𝐴 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐺
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem undifixp
StepHypRef Expression
1 unexg 7106 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → (𝐹𝐺) ∈ V)
213adant3 1126 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ V)
3 ixpfn 8068 . . . 4 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐺 Fn (𝐴𝐵))
4 ixpfn 8068 . . . 4 (𝐹X𝑥𝐵 𝐶𝐹 Fn 𝐵)
5 3simpa 1142 . . . . . . . 8 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵))
65ancomd 453 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)))
7 disjdif 4182 . . . . . . 7 (𝐵 ∩ (𝐴𝐵)) = ∅
8 fnun 6137 . . . . . . 7 (((𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)) ∧ (𝐵 ∩ (𝐴𝐵)) = ∅) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
96, 7, 8sylancl 574 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
10 undif 4191 . . . . . . . . . 10 (𝐵𝐴 ↔ (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1110biimpi 206 . . . . . . . . 9 (𝐵𝐴 → (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1211eqcomd 2777 . . . . . . . 8 (𝐵𝐴𝐴 = (𝐵 ∪ (𝐴𝐵)))
13123ad2ant3 1129 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → 𝐴 = (𝐵 ∪ (𝐴𝐵)))
1413fneq2d 6122 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → ((𝐹𝐺) Fn 𝐴 ↔ (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵))))
159, 14mpbird 247 . . . . 5 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
16153exp 1112 . . . 4 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
173, 4, 16syl2imc 41 . . 3 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
18173imp 1101 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
19 elixp2 8066 . . . . . . . . . . . . 13 (𝐹X𝑥𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶))
2019simp3bi 1141 . . . . . . . . . . . 12 (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶)
21 fndm 6130 . . . . . . . . . . . . . 14 (𝐺 Fn (𝐴𝐵) → dom 𝐺 = (𝐴𝐵))
22 elndif 3885 . . . . . . . . . . . . . 14 (𝑥𝐵 → ¬ 𝑥 ∈ (𝐴𝐵))
23 eleq2 2839 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ dom 𝐺))
2423notbid 307 . . . . . . . . . . . . . . . 16 ((𝐴𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
2524eqcoms 2779 . . . . . . . . . . . . . . 15 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26 ndmfv 6359 . . . . . . . . . . . . . . 15 𝑥 ∈ dom 𝐺 → (𝐺𝑥) = ∅)
2725, 26syl6bi 243 . . . . . . . . . . . . . 14 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) → (𝐺𝑥) = ∅))
2821, 22, 27syl2im 40 . . . . . . . . . . . . 13 (𝐺 Fn (𝐴𝐵) → (𝑥𝐵 → (𝐺𝑥) = ∅))
2928ralrimiv 3114 . . . . . . . . . . . 12 (𝐺 Fn (𝐴𝐵) → ∀𝑥𝐵 (𝐺𝑥) = ∅)
30 uneq2 3912 . . . . . . . . . . . . . . 15 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅))
31 un0 4111 . . . . . . . . . . . . . . 15 ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)
32 eqtr 2790 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥))
33 eleq1 2838 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3433biimpd 219 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3534eqcoms 2779 . . . . . . . . . . . . . . . 16 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3632, 35syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3730, 31, 36sylancl 574 . . . . . . . . . . . . . 14 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3837com12 32 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ 𝐶 → ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3938ral2imi 3096 . . . . . . . . . . . 12 (∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶 → (∀𝑥𝐵 (𝐺𝑥) = ∅ → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4020, 29, 39syl2imc 41 . . . . . . . . . . 11 (𝐺 Fn (𝐴𝐵) → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
413, 40syl 17 . . . . . . . . . 10 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4241impcom 394 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
43 elixp2 8066 . . . . . . . . . . . . 13 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴𝐵) ∧ ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶))
4443simp3bi 1141 . . . . . . . . . . . 12 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶)
45 fndm 6130 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46 eldifn 3884 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴𝐵) → ¬ 𝑥𝐵)
47 eleq2 2839 . . . . . . . . . . . . . . . . 17 (𝐵 = dom 𝐹 → (𝑥𝐵𝑥 ∈ dom 𝐹))
4847notbid 307 . . . . . . . . . . . . . . . 16 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49 ndmfv 6359 . . . . . . . . . . . . . . . 16 𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ∅)
5048, 49syl6bi 243 . . . . . . . . . . . . . . 15 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5150eqcoms 2779 . . . . . . . . . . . . . 14 (dom 𝐹 = 𝐵 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5245, 46, 51syl2im 40 . . . . . . . . . . . . 13 (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴𝐵) → (𝐹𝑥) = ∅))
5352ralrimiv 3114 . . . . . . . . . . . 12 (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅)
54 uneq1 3911 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)))
55 uncom 3908 . . . . . . . . . . . . . . 15 (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)
56 eqtr 2790 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅))
57 un0 4111 . . . . . . . . . . . . . . . 16 ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)
58 eqtr 2790 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥))
59 eleq1 2838 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6059biimpd 219 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6160eqcoms 2779 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6258, 61syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6356, 57, 62sylancl 574 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6454, 55, 63sylancl 574 . . . . . . . . . . . . . 14 ((𝐹𝑥) = ∅ → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6564com12 32 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6665ral2imi 3096 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6744, 53, 66syl2imc 41 . . . . . . . . . . 11 (𝐹 Fn 𝐵 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
684, 67syl 17 . . . . . . . . . 10 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6968imp 393 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
70 ralunb 3945 . . . . . . . . 9 (∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ (∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7142, 69, 70sylanbrc 572 . . . . . . . 8 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
7271ex 397 . . . . . . 7 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
73 raleq 3287 . . . . . . . 8 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7473imbi2d 329 . . . . . . 7 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → ((𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶) ↔ (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7572, 74syl5ibr 236 . . . . . 6 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7675eqcoms 2779 . . . . 5 ((𝐵 ∪ (𝐴𝐵)) = 𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7710, 76sylbi 207 . . . 4 (𝐵𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
78773imp231 1104 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
79 df-fn 6034 . . . . . 6 (𝐺 Fn (𝐴𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)))
80 df-fn 6034 . . . . . . . 8 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81 simpl 468 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82 simpl 468 . . . . . . . . . . . . . 14 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → Fun 𝐺)
8381, 82anim12i 600 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84833adant3 1126 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85 ineq12 3960 . . . . . . . . . . . . . . 15 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴𝐵)))
8685, 7syl6eq 2821 . . . . . . . . . . . . . 14 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
8786ad2ant2l 740 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88873adant3 1126 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89 fvun 6410 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9084, 88, 89syl2anc 573 . . . . . . . . . . 11 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9190eleq1d 2835 . . . . . . . . . 10 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9291ralbidv 3135 . . . . . . . . 9 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
93923exp 1112 . . . . . . . 8 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9480, 93sylbi 207 . . . . . . 7 (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9594com12 32 . . . . . 6 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9679, 95sylbi 207 . . . . 5 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
973, 4, 96syl2imc 41 . . . 4 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
98973imp 1101 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9978, 98mpbird 247 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶)
100 elixp2 8066 . 2 ((𝐹𝐺) ∈ X𝑥𝐴 𝐶 ↔ ((𝐹𝐺) ∈ V ∧ (𝐹𝐺) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶))
1012, 18, 99, 100syl3anbrc 1428 1 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  dom cdm 5249  Fun wfun 6025   Fn wfn 6026  cfv 6031  Xcixp 8062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-fv 6039  df-ixp 8063
This theorem is referenced by:  ptuncnv  21831  ptunhmeo  21832
  Copyright terms: Public domain W3C validator