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

Theorem undifixp 8962
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 7756 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → (𝐹𝐺) ∈ V)
213adant3 1129 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ V)
3 ixpfn 8931 . . . 4 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐺 Fn (𝐴𝐵))
4 ixpfn 8931 . . . 4 (𝐹X𝑥𝐵 𝐶𝐹 Fn 𝐵)
5 3simpa 1145 . . . . . . . 8 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵))
65ancomd 460 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)))
7 disjdif 4475 . . . . . . 7 (𝐵 ∩ (𝐴𝐵)) = ∅
8 fnun 6673 . . . . . . 7 (((𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)) ∧ (𝐵 ∩ (𝐴𝐵)) = ∅) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
96, 7, 8sylancl 584 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
10 undif 4485 . . . . . . . . . 10 (𝐵𝐴 ↔ (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1110biimpi 215 . . . . . . . . 9 (𝐵𝐴 → (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1211eqcomd 2731 . . . . . . . 8 (𝐵𝐴𝐴 = (𝐵 ∪ (𝐴𝐵)))
13123ad2ant3 1132 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → 𝐴 = (𝐵 ∪ (𝐴𝐵)))
1413fneq2d 6653 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → ((𝐹𝐺) Fn 𝐴 ↔ (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵))))
159, 14mpbird 256 . . . . 5 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
16153exp 1116 . . . 4 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
173, 4, 16syl2imc 41 . . 3 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
18173imp 1108 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
19 elixp2 8929 . . . . . . . . . . . . 13 (𝐹X𝑥𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶))
2019simp3bi 1144 . . . . . . . . . . . 12 (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶)
21 fndm 6662 . . . . . . . . . . . . . 14 (𝐺 Fn (𝐴𝐵) → dom 𝐺 = (𝐴𝐵))
22 elndif 4127 . . . . . . . . . . . . . 14 (𝑥𝐵 → ¬ 𝑥 ∈ (𝐴𝐵))
23 eleq2 2814 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ dom 𝐺))
2423notbid 317 . . . . . . . . . . . . . . . 16 ((𝐴𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
2524eqcoms 2733 . . . . . . . . . . . . . . 15 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26 ndmfv 6935 . . . . . . . . . . . . . . 15 𝑥 ∈ dom 𝐺 → (𝐺𝑥) = ∅)
2725, 26biimtrdi 252 . . . . . . . . . . . . . 14 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) → (𝐺𝑥) = ∅))
2821, 22, 27syl2im 40 . . . . . . . . . . . . 13 (𝐺 Fn (𝐴𝐵) → (𝑥𝐵 → (𝐺𝑥) = ∅))
2928ralrimiv 3134 . . . . . . . . . . . 12 (𝐺 Fn (𝐴𝐵) → ∀𝑥𝐵 (𝐺𝑥) = ∅)
30 uneq2 4156 . . . . . . . . . . . . . . 15 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅))
31 un0 4394 . . . . . . . . . . . . . . 15 ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)
32 eqtr 2748 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥))
33 eleq1 2813 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3433biimpd 228 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3534eqcoms 2733 . . . . . . . . . . . . . . . 16 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3632, 35syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3730, 31, 36sylancl 584 . . . . . . . . . . . . . 14 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3837com12 32 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ 𝐶 → ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3938ral2imi 3074 . . . . . . . . . . . 12 (∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶 → (∀𝑥𝐵 (𝐺𝑥) = ∅ → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4020, 29, 39syl2imc 41 . . . . . . . . . . 11 (𝐺 Fn (𝐴𝐵) → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
413, 40syl 17 . . . . . . . . . 10 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4241impcom 406 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
43 elixp2 8929 . . . . . . . . . . . . 13 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴𝐵) ∧ ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶))
4443simp3bi 1144 . . . . . . . . . . . 12 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶)
45 fndm 6662 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46 eldifn 4126 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴𝐵) → ¬ 𝑥𝐵)
47 eleq2 2814 . . . . . . . . . . . . . . . . 17 (𝐵 = dom 𝐹 → (𝑥𝐵𝑥 ∈ dom 𝐹))
4847notbid 317 . . . . . . . . . . . . . . . 16 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49 ndmfv 6935 . . . . . . . . . . . . . . . 16 𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ∅)
5048, 49biimtrdi 252 . . . . . . . . . . . . . . 15 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5150eqcoms 2733 . . . . . . . . . . . . . 14 (dom 𝐹 = 𝐵 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5245, 46, 51syl2im 40 . . . . . . . . . . . . 13 (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴𝐵) → (𝐹𝑥) = ∅))
5352ralrimiv 3134 . . . . . . . . . . . 12 (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅)
54 uneq1 4155 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)))
55 uncom 4152 . . . . . . . . . . . . . . 15 (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)
56 eqtr 2748 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅))
57 un0 4394 . . . . . . . . . . . . . . . 16 ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)
58 eqtr 2748 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥))
59 eleq1 2813 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6059biimpd 228 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6160eqcoms 2733 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6258, 61syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6356, 57, 62sylancl 584 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6454, 55, 63sylancl 584 . . . . . . . . . . . . . 14 ((𝐹𝑥) = ∅ → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6564com12 32 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6665ral2imi 3074 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6744, 53, 66syl2imc 41 . . . . . . . . . . 11 (𝐹 Fn 𝐵 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
684, 67syl 17 . . . . . . . . . 10 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6968imp 405 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
70 ralunb 4191 . . . . . . . . 9 (∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ (∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7142, 69, 70sylanbrc 581 . . . . . . . 8 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
7271ex 411 . . . . . . 7 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
73 raleq 3311 . . . . . . . 8 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7473imbi2d 339 . . . . . . 7 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → ((𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶) ↔ (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7572, 74imbitrrid 245 . . . . . 6 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7675eqcoms 2733 . . . . 5 ((𝐵 ∪ (𝐴𝐵)) = 𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7710, 76sylbi 216 . . . 4 (𝐵𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
78773imp231 1110 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
79 df-fn 6556 . . . . . 6 (𝐺 Fn (𝐴𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)))
80 df-fn 6556 . . . . . . . 8 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81 simpl 481 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82 simpl 481 . . . . . . . . . . . . . 14 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → Fun 𝐺)
8381, 82anim12i 611 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84833adant3 1129 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85 ineq12 4207 . . . . . . . . . . . . . . 15 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴𝐵)))
8685, 7eqtrdi 2781 . . . . . . . . . . . . . 14 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
8786ad2ant2l 744 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88873adant3 1129 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89 fvun 6991 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9084, 88, 89syl2anc 582 . . . . . . . . . . 11 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9190eleq1d 2810 . . . . . . . . . 10 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9291ralbidv 3167 . . . . . . . . 9 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
93923exp 1116 . . . . . . . 8 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9480, 93sylbi 216 . . . . . . 7 (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9594com12 32 . . . . . 6 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9679, 95sylbi 216 . . . . 5 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
973, 4, 96syl2imc 41 . . . 4 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
98973imp 1108 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9978, 98mpbird 256 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶)
100 elixp2 8929 . 2 ((𝐹𝐺) ∈ X𝑥𝐴 𝐶 ↔ ((𝐹𝐺) ∈ V ∧ (𝐹𝐺) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶))
1012, 18, 99, 100syl3anbrc 1340 1 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ X𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  cdif 3943  cun 3944  cin 3945  wss 3946  c0 4324  dom cdm 5681  Fun wfun 6547   Fn wfn 6548  cfv 6553  Xcixp 8925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561  df-ixp 8926
This theorem is referenced by:  ptuncnv  23794  ptunhmeo  23795
  Copyright terms: Public domain W3C validator