undifixp - Metamath Proof Explorer

	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**
Step	Hyp	Ref	Expression
1		unexg 7756	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → (𝐹 ∪ 𝐺) ∈ V)
2	1	3adant3 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 𝐵))
6	5	ancomd 460	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)))
7		disjdif 4475	. . . . . . 7 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅
8		fnun 6673	. . . . . . 7 ⊢ (((𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)) ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
9	6, 7, 8	sylancl 584	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
10		undif 4485	. . . . . . . . . 10 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
11	10	biimpi 215	. . . . . . . . 9 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
12	11	eqcomd 2731	. . . . . . . 8 ⊢ (𝐵 ⊆ 𝐴 → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
13	12	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
14	13	fneq2d 6653	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺) Fn 𝐴 ↔ (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))))
15	9, 14	mpbird 256	. . . . 5 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
16	15	3exp 1116	. . . 4 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
17	3, 4, 16	syl2imc 41	. . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
18	17	3imp 1108	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
19		elixp2 8929	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶))
20	19	simp3bi 1144	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶)
21		fndm 6662	. . . . . . . . . . . . . 14 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → dom 𝐺 = (𝐴 ∖ 𝐵))
22		elndif 4127	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
23		eleq2 2814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 𝑥 ∈ dom 𝐺))
24	23	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
25	24	eqcoms 2733	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26		ndmfv 6935	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) = ∅)
27	25, 26	biimtrdi 252	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐺‘𝑥) = ∅))
28	21, 22, 27	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐵 → (𝐺‘𝑥) = ∅))
29	28	ralrimiv 3134	. . . . . . . . . . . 12 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅)
30		uneq2 4156	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅))
31		un0 4394	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)
32		eqtr 2748	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥))
33		eleq1 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
34	33	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
35	34	eqcoms 2733	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
36	32, 35	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
37	30, 31, 36	sylancl 584	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
38	37	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ 𝐶 → ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
39	38	ral2imi 3074	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
40	20, 29, 39	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
41	3, 40	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
42	41	impcom 406	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
43		elixp2 8929	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 ∖ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶))
44	43	simp3bi 1144	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶)
45		fndm 6662	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46		eldifn 4126	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
47		eleq2 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = dom 𝐹 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹))
48	47	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49		ndmfv 6935	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ∅)
50	48, 49	biimtrdi 252	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
51	50	eqcoms 2733	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 = 𝐵 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
52	45, 46, 51	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐹‘𝑥) = ∅))
53	52	ralrimiv 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 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
60	59	biimpd 228	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
61	60	eqcoms 2733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
63	56, 57, 62	sylancl 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
64	54, 55, 63	sylancl 584	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
65	64	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
66	65	ral2imi 3074	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
67	44, 53, 66	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐵 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
68	4, 67	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
69	68	imp 405	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
70		ralunb 4191	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ (∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
71	42, 69, 70	sylanbrc 581	. . . . . . . 8 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
72	71	ex 411	. . . . . . 7 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
73		raleq 3311	. . . . . . . 8 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
74	73	imbi2d 339	. . . . . . 7 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → ((𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) ↔ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
75	72, 74	imbitrrid 245	. . . . . 6 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
76	75	eqcoms 2733	. . . . 5 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
77	10, 76	sylbi 216	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
78	77	3imp231 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 𝐺)
83	81, 82	anim12i 611	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84	83	3adant3 1129	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85		ineq12 4207	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴 ∖ 𝐵)))
86	85, 7	eqtrdi 2781	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
87	86	ad2ant2l 744	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88	87	3adant3 1129	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89		fvun 6991	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
90	84, 88, 89	syl2anc 582	. . . . . . . . . . 11 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
91	90	eleq1d 2810	. . . . . . . . . 10 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
92	91	ralbidv 3167	. . . . . . . . 9 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
93	92	3exp 1116	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
94	80, 93	sylbi 216	. . . . . . 7 ⊢ (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
95	94	com12 32	. . . . . 6 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
96	79, 95	sylbi 216	. . . . 5 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
97	3, 4, 96	syl2imc 41	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
98	97	3imp 1108	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
99	78, 98	mpbird 256	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶)
100		elixp2 8929	. 2 ⊢ ((𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶 ↔ ((𝐹 ∪ 𝐺) ∈ V ∧ (𝐹 ∪ 𝐺) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶))
101	2, 18, 99, 100	syl3anbrc 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

W3C validator