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

Theorem undifixp 7830
 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 6857 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → (𝐹𝐺) ∈ V)
213adant3 1074 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ V)
3 ixpfn 7800 . . . 4 (𝐹X𝑥𝐵 𝐶𝐹 Fn 𝐵)
4 ixpfn 7800 . . . . 5 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐺 Fn (𝐴𝐵))
5 3simpa 1051 . . . . . . . . 9 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵))
65ancomd 466 . . . . . . . 8 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)))
7 disjdif 3992 . . . . . . . 8 (𝐵 ∩ (𝐴𝐵)) = ∅
8 fnun 5911 . . . . . . . 8 (((𝐹 Fn 𝐵𝐺 Fn (𝐴𝐵)) ∧ (𝐵 ∩ (𝐴𝐵)) = ∅) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
96, 7, 8sylancl 693 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵)))
10 undif 4001 . . . . . . . . . . 11 (𝐵𝐴 ↔ (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1110biimpi 205 . . . . . . . . . 10 (𝐵𝐴 → (𝐵 ∪ (𝐴𝐵)) = 𝐴)
1211eqcomd 2616 . . . . . . . . 9 (𝐵𝐴𝐴 = (𝐵 ∪ (𝐴𝐵)))
13123ad2ant3 1077 . . . . . . . 8 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → 𝐴 = (𝐵 ∪ (𝐴𝐵)))
1413fneq2d 5896 . . . . . . 7 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → ((𝐹𝐺) Fn 𝐴 ↔ (𝐹𝐺) Fn (𝐵 ∪ (𝐴𝐵))))
159, 14mpbird 246 . . . . . 6 ((𝐺 Fn (𝐴𝐵) ∧ 𝐹 Fn 𝐵𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
16153exp 1256 . . . . 5 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
174, 16syl 17 . . . 4 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹 Fn 𝐵 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
183, 17syl5com 31 . . 3 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (𝐹𝐺) Fn 𝐴)))
19183imp 1249 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) Fn 𝐴)
20 fndm 5904 . . . . . . . . . . . . . . 15 (𝐺 Fn (𝐴𝐵) → dom 𝐺 = (𝐴𝐵))
21 elndif 3696 . . . . . . . . . . . . . . 15 (𝑥𝐵 → ¬ 𝑥 ∈ (𝐴𝐵))
22 eleq2 2677 . . . . . . . . . . . . . . . . . 18 ((𝐴𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ dom 𝐺))
2322notbid 307 . . . . . . . . . . . . . . . . 17 ((𝐴𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
2423eqcoms 2618 . . . . . . . . . . . . . . . 16 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
25 ndmfv 6128 . . . . . . . . . . . . . . . 16 𝑥 ∈ dom 𝐺 → (𝐺𝑥) = ∅)
2624, 25syl6bi 242 . . . . . . . . . . . . . . 15 (dom 𝐺 = (𝐴𝐵) → (¬ 𝑥 ∈ (𝐴𝐵) → (𝐺𝑥) = ∅))
2720, 21, 26syl2im 39 . . . . . . . . . . . . . 14 (𝐺 Fn (𝐴𝐵) → (𝑥𝐵 → (𝐺𝑥) = ∅))
2827ralrimiv 2948 . . . . . . . . . . . . 13 (𝐺 Fn (𝐴𝐵) → ∀𝑥𝐵 (𝐺𝑥) = ∅)
29 elixp2 7798 . . . . . . . . . . . . . . 15 (𝐹X𝑥𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶))
3029simp3bi 1071 . . . . . . . . . . . . . 14 (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶)
31 uneq2 3723 . . . . . . . . . . . . . . . . 17 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅))
32 un0 3919 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)
33 eqtr 2629 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥))
34 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3534biimpd 218 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3635eqcoms 2618 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐹𝑥) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3733, 36syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐹𝑥) ∪ ∅) ∧ ((𝐹𝑥) ∪ ∅) = (𝐹𝑥)) → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3831, 32, 37sylancl 693 . . . . . . . . . . . . . . . 16 ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
3938com12 32 . . . . . . . . . . . . . . 15 ((𝐹𝑥) ∈ 𝐶 → ((𝐺𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4039ral2imi 2931 . . . . . . . . . . . . . 14 (∀𝑥𝐵 (𝐹𝑥) ∈ 𝐶 → (∀𝑥𝐵 (𝐺𝑥) = ∅ → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4130, 40syl 17 . . . . . . . . . . . . 13 (𝐹X𝑥𝐵 𝐶 → (∀𝑥𝐵 (𝐺𝑥) = ∅ → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4228, 41syl5com 31 . . . . . . . . . . . 12 (𝐺 Fn (𝐴𝐵) → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
434, 42syl 17 . . . . . . . . . . 11 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹X𝑥𝐵 𝐶 → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
4443impcom 445 . . . . . . . . . 10 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
45 fndm 5904 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46 eldifn 3695 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴𝐵) → ¬ 𝑥𝐵)
47 eleq2 2677 . . . . . . . . . . . . . . . . . 18 (𝐵 = dom 𝐹 → (𝑥𝐵𝑥 ∈ dom 𝐹))
4847notbid 307 . . . . . . . . . . . . . . . . 17 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49 ndmfv 6128 . . . . . . . . . . . . . . . . 17 𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ∅)
5048, 49syl6bi 242 . . . . . . . . . . . . . . . 16 (𝐵 = dom 𝐹 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5150eqcoms 2618 . . . . . . . . . . . . . . 15 (dom 𝐹 = 𝐵 → (¬ 𝑥𝐵 → (𝐹𝑥) = ∅))
5245, 46, 51syl2im 39 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴𝐵) → (𝐹𝑥) = ∅))
5352ralrimiv 2948 . . . . . . . . . . . . 13 (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅)
54 elixp2 7798 . . . . . . . . . . . . . . 15 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴𝐵) ∧ ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶))
5554simp3bi 1071 . . . . . . . . . . . . . 14 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶)
56 uneq1 3722 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)))
57 uncom 3719 . . . . . . . . . . . . . . . . 17 (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)
58 eqtr 2629 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅))
59 un0 3919 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)
60 eqtr 2629 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥))
61 eleq1 2676 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6261biimpd 218 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6362eqcoms 2618 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑥) ∪ (𝐺𝑥)) = (𝐺𝑥) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6460, 63syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑥) ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅) ∧ ((𝐺𝑥) ∪ ∅) = (𝐺𝑥)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6558, 59, 64sylancl 693 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑥) ∪ (𝐺𝑥)) = (∅ ∪ (𝐺𝑥)) ∧ (∅ ∪ (𝐺𝑥)) = ((𝐺𝑥) ∪ ∅)) → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6656, 57, 65sylancl 693 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) = ∅ → ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6766com12 32 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → ((𝐹𝑥) = ∅ → ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6867ral2imi 2931 . . . . . . . . . . . . . 14 (∀𝑥 ∈ (𝐴𝐵)(𝐺𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
6955, 68syl 17 . . . . . . . . . . . . 13 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (∀𝑥 ∈ (𝐴𝐵)(𝐹𝑥) = ∅ → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7053, 69syl5com 31 . . . . . . . . . . . 12 (𝐹 Fn 𝐵 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
713, 70syl 17 . . . . . . . . . . 11 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7271imp 444 . . . . . . . . . 10 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
73 ralunb 3756 . . . . . . . . . 10 (∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ (∀𝑥𝐵 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴𝐵)((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7444, 72, 73sylanbrc 695 . . . . . . . . 9 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
7574ex 449 . . . . . . . 8 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
76 raleq 3115 . . . . . . . . 9 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
7776imbi2d 329 . . . . . . . 8 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → ((𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶) ↔ (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴𝐵))((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7875, 77syl5ibr 235 . . . . . . 7 (𝐴 = (𝐵 ∪ (𝐴𝐵)) → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
7978eqcoms 2618 . . . . . 6 ((𝐵 ∪ (𝐴𝐵)) = 𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
8010, 79sylbi 206 . . . . 5 (𝐵𝐴 → (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
8180com3l 87 . . . 4 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)))
82813imp 1249 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶)
83 df-fn 5807 . . . . . . 7 (𝐺 Fn (𝐴𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)))
84 df-fn 5807 . . . . . . . . 9 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
85 simpl 472 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
86 simpl 472 . . . . . . . . . . . . . . 15 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → Fun 𝐺)
8785, 86anim12i 588 . . . . . . . . . . . . . 14 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
88873adant3 1074 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
89 ineq12 3771 . . . . . . . . . . . . . . . 16 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴𝐵)))
9089, 7syl6eq 2660 . . . . . . . . . . . . . . 15 ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
9190ad2ant2l 778 . . . . . . . . . . . . . 14 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
92913adant3 1074 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
93 fvun 6178 . . . . . . . . . . . . 13 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9488, 92, 93syl2anc 691 . . . . . . . . . . . 12 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → ((𝐹𝐺)‘𝑥) = ((𝐹𝑥) ∪ (𝐺𝑥)))
9594eleq1d 2672 . . . . . . . . . . 11 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
9695ralbidv 2969 . . . . . . . . . 10 (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) ∧ 𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
97963exp 1256 . . . . . . . . 9 ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9884, 97sylbi 206 . . . . . . . 8 (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
9998com12 32 . . . . . . 7 ((Fun 𝐺 ∧ dom 𝐺 = (𝐴𝐵)) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
10083, 99sylbi 206 . . . . . 6 (𝐺 Fn (𝐴𝐵) → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
1014, 100syl 17 . . . . 5 (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐹 Fn 𝐵 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
1023, 101syl5com 31 . . . 4 (𝐹X𝑥𝐵 𝐶 → (𝐺X𝑥 ∈ (𝐴𝐵)𝐶 → (𝐵𝐴 → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))))
1031023imp 1249 . . 3 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥𝐴 ((𝐹𝑥) ∪ (𝐺𝑥)) ∈ 𝐶))
10482, 103mpbird 246 . 2 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶)
105 elixp2 7798 . 2 ((𝐹𝐺) ∈ X𝑥𝐴 𝐶 ↔ ((𝐹𝐺) ∈ V ∧ (𝐹𝐺) Fn 𝐴 ∧ ∀𝑥𝐴 ((𝐹𝐺)‘𝑥) ∈ 𝐶))
1062, 19, 104, 105syl3anbrc 1239 1 ((𝐹X𝑥𝐵 𝐶𝐺X𝑥 ∈ (𝐴𝐵)𝐶𝐵𝐴) → (𝐹𝐺) ∈ X𝑥𝐴 𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  dom cdm 5038  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  Xcixp 7794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-ixp 7795 This theorem is referenced by:  ptuncnv  21420  ptunhmeo  21421
 Copyright terms: Public domain W3C validator