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

Theorem undifixp 8485
 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 7456 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → (𝐹𝐺) ∈ V)
213adant3 1129 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ V)
3 ixpfn 8454 . . . 4 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐺 Fn (𝐴𝐵))
4 ixpfn 8454 . . . 4 (𝐹X𝑥𝐵 𝐶𝐹 Fn 𝐵)
5 3simpa 1145 . . . . . . . 8 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵))
65ancomd 465 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)))
7 disjdif 4382 . . . . . . 7 (𝐵 ∩ (𝐴𝐵)) = ∅
8 fnun 6438 . . . . . . 7 (((𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)) ∧ (𝐵 ∩ (𝐴𝐵)) = ∅) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
96, 7, 8sylancl 589 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
10 undif 4391 . . . . . . . . . 10 (𝐵𝐴 ↔ (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1110biimpi 219 . . . . . . . . 9 (𝐵𝐴 → (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1211eqcomd 2807 . . . . . . . 8 (𝐵𝐴𝐴 = (𝐵 ∪ (𝐴𝐵)))
13123ad2ant3 1132 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → 𝐴 = (𝐵 ∪ (𝐴𝐵)))
1413fneq2d 6421 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → ((𝐹𝐺) Fn 𝐴 ↔ (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵))))
159, 14mpbird 260 . . . . 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 8452 . . . . . . . . . . . . 13 (𝐹X𝑥𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶))
2019simp3bi 1144 . . . . . . . . . . . 12 (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶)
21 fndm 6429 . . . . . . . . . . . . . 14 (𝐺 Fn (𝐴𝐵) → dom 𝐺 = (𝐴𝐵))
22 elndif 4059 . . . . . . . . . . . . . 14 (𝑥𝐵 → ¬ 𝑥 ∈ (𝐴𝐵))
23 eleq2 2881 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ dom 𝐺))
2423notbid 321 . . . . . . . . . . . . . . . 16 ((𝐴𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
2524eqcoms 2809 . . . . . . . . . . . . . . 15 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26 ndmfv 6679 . . . . . . . . . . . . . . 15 𝑥 ∈ dom 𝐺 → (𝐺𝑥) = ∅)
2725, 26syl6bi 256 . . . . . . . . . . . . . 14 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) → (𝐺𝑥) = ∅))
2821, 22, 27syl2im 40 . . . . . . . . . . . . 13 (𝐺 Fn (𝐴𝐵) → (𝑥𝐵 → (𝐺𝑥) = ∅))
2928ralrimiv 3151 . . . . . . . . . . . 12 (𝐺 Fn (𝐴𝐵) → ∀𝑥𝐵 (𝐺𝑥) = ∅)
30 uneq2 4087 . . . . . . . . . . . . . . 15 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅))
31 un0 4301 . . . . . . . . . . . . . . 15 ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)
32 eqtr 2821 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥))
33 eleq1 2880 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3433biimpd 232 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3534eqcoms 2809 . . . . . . . . . . . . . . . 16 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3632, 35syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3730, 31, 36sylancl 589 . . . . . . . . . . . . . 14 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3837com12 32 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ 𝐶 → ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3938ral2imi 3127 . . . . . . . . . . . 12 (∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶 → (∀𝑥𝐵 (𝐺𝑥) = ∅ → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4020, 29, 39syl2imc 41 . . . . . . . . . . 11 (𝐺 Fn (𝐴𝐵) → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
413, 40syl 17 . . . . . . . . . 10 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4241impcom 411 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
43 elixp2 8452 . . . . . . . . . . . . 13 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴𝐵) ∧ ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶))
4443simp3bi 1144 . . . . . . . . . . . 12 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶)
45 fndm 6429 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46 eldifn 4058 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴𝐵) → ¬ 𝑥𝐵)
47 eleq2 2881 . . . . . . . . . . . . . . . . 17 (𝐵 = dom 𝐹 → (𝑥𝐵𝑥 ∈ dom 𝐹))
4847notbid 321 . . . . . . . . . . . . . . . 16 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49 ndmfv 6679 . . . . . . . . . . . . . . . 16 𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ∅)
5048, 49syl6bi 256 . . . . . . . . . . . . . . 15 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5150eqcoms 2809 . . . . . . . . . . . . . 14 (dom 𝐹 = 𝐵 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5245, 46, 51syl2im 40 . . . . . . . . . . . . 13 (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴𝐵) → (𝐹𝑥) = ∅))
5352ralrimiv 3151 . . . . . . . . . . . 12 (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅)
54 uneq1 4086 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)))
55 uncom 4083 . . . . . . . . . . . . . . 15 (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)
56 eqtr 2821 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅))
57 un0 4301 . . . . . . . . . . . . . . . 16 ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)
58 eqtr 2821 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥))
59 eleq1 2880 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6059biimpd 232 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6160eqcoms 2809 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6258, 61syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6356, 57, 62sylancl 589 . . . . . . . . . . . . . . 15 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6454, 55, 63sylancl 589 . . . . . . . . . . . . . 14 ((𝐹𝑥) = ∅ → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6564com12 32 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6665ral2imi 3127 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6744, 53, 66syl2imc 41 . . . . . . . . . . 11 (𝐹 Fn 𝐵 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
684, 67syl 17 . . . . . . . . . 10 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6968imp 410 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
70 ralunb 4121 . . . . . . . . 9 (∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ (∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7142, 69, 70sylanbrc 586 . . . . . . . 8 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
7271ex 416 . . . . . . 7 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
73 raleq 3361 . . . . . . . 8 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7473imbi2d 344 . . . . . . 7 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → ((𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶) ↔ (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7572, 74syl5ibr 249 . . . . . 6 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7675eqcoms 2809 . . . . 5 ((𝐵 ∪ (𝐴𝐵)) = 𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7710, 76sylbi 220 . . . 4 (𝐵𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
78773imp231 1110 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
79 df-fn 6331 . . . . . 6 (𝐺 Fn (𝐴𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)))
80 df-fn 6331 . . . . . . . 8 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81 simpl 486 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82 simpl 486 . . . . . . . . . . . . . 14 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → Fun 𝐺)
8381, 82anim12i 615 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84833adant3 1129 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85 ineq12 4137 . . . . . . . . . . . . . . 15 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴𝐵)))
8685, 7eqtrdi 2852 . . . . . . . . . . . . . 14 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
8786ad2ant2l 745 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88873adant3 1129 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89 fvun 6732 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9084, 88, 89syl2anc 587 . . . . . . . . . . 11 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9190eleq1d 2877 . . . . . . . . . 10 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9291ralbidv 3165 . . . . . . . . 9 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
93923exp 1116 . . . . . . . 8 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9480, 93sylbi 220 . . . . . . 7 (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9594com12 32 . . . . . 6 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9679, 95sylbi 220 . . . . 5 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
973, 4, 96syl2imc 41 . . . 4 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
98973imp 1108 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9978, 98mpbird 260 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶)
100 elixp2 8452 . 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 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  ∀wral 3109  Vcvv 3444   ∖ cdif 3881   ∪ cun 3882   ∩ cin 3883   ⊆ wss 3884  ∅c0 4246  dom cdm 5523  Fun wfun 6322   Fn wfn 6323  ‘cfv 6328  Xcixp 8448 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-fv 6336  df-ixp 8449 This theorem is referenced by:  ptuncnv  22415  ptunhmeo  22416
 Copyright terms: Public domain W3C validator