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 8879

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 7693	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → (𝐹 ∪ 𝐺) ∈ V)
2	1	3adant3 1138	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ V)
3		ixpfn 8848	. . . 4 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → 𝐺 Fn (𝐴 ∖ 𝐵))
4		ixpfn 8848	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → 𝐹 Fn 𝐵)
5		3simpa 1154	. . . . . . . 8 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵))
6	5	ancomd 462	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)))
7		disjdif 4407	. . . . . . 7 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅
8		fnun 6606	. . . . . . 7 ⊢ (((𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)) ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
9	6, 7, 8	sylancl 592	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
10		undif 4417	. . . . . . . . . 10 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
11	10	biimpi 217	. . . . . . . . 9 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
12	11	eqcomd 2746	. . . . . . . 8 ⊢ (𝐵 ⊆ 𝐴 → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
13	12	3ad2ant3 1141	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
14	13	fneq2d 6586	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺) Fn 𝐴 ↔ (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))))
15	9, 14	mpbird 258	. . . . 5 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
16	15	3exp 1125	. . . 4 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
17	3, 4, 16	syl2imc 41	. . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
18	17	3imp 1116	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
19		elixp2 8846	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶))
20	19	simp3bi 1153	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶)
21		fndm 6595	. . . . . . . . . . . . . 14 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → dom 𝐺 = (𝐴 ∖ 𝐵))
22		elndif 4070	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
23		eleq2 2829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 𝑥 ∈ dom 𝐺))
24	23	notbid 319	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
25	24	eqcoms 2748	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26		ndmfv 6866	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) = ∅)
27	25, 26	biimtrdi 254	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐺‘𝑥) = ∅))
28	21, 22, 27	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐵 → (𝐺‘𝑥) = ∅))
29	28	ralrimiv 3131	. . . . . . . . . . . 12 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅)
30		uneq2 4099	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅))
31		un0 4329	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)
32		eqtr 2760	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥))
33		eleq1 2828	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
34	33	biimpd 230	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
35	34	eqcoms 2748	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
36	32, 35	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
37	30, 31, 36	sylancl 592	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
38	37	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ 𝐶 → ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
39	38	ral2imi 3079	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
40	20, 29, 39	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
41	3, 40	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
42	41	impcom 408	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
43		elixp2 8846	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 ∖ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶))
44	43	simp3bi 1153	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶)
45		fndm 6595	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46		eldifn 4069	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
47		eleq2 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = dom 𝐹 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹))
48	47	notbid 319	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49		ndmfv 6866	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ∅)
50	48, 49	biimtrdi 254	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
51	50	eqcoms 2748	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 = 𝐵 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
52	45, 46, 51	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐹‘𝑥) = ∅))
53	52	ralrimiv 3131	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅)
54		uneq1 4098	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)))
55		uncom 4095	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)
56		eqtr 2760	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅))
57		un0 4329	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)
58		eqtr 2760	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥))
59		eleq1 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
60	59	biimpd 230	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
61	60	eqcoms 2748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
63	56, 57, 62	sylancl 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
64	54, 55, 63	sylancl 592	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
65	64	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
66	65	ral2imi 3079	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
67	44, 53, 66	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐵 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
68	4, 67	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
69	68	imp 407	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
70		ralunb 4133	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ (∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
71	42, 69, 70	sylanbrc 589	. . . . . . . 8 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
72	71	ex 413	. . . . . . 7 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
73		raleq 3295	. . . . . . . 8 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
74	73	imbi2d 341	. . . . . . 7 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → ((𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) ↔ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
75	72, 74	imbitrrid 247	. . . . . 6 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
76	75	eqcoms 2748	. . . . 5 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
77	10, 76	sylbi 218	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
78	77	3imp231 1118	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
79		df-fn 6495	. . . . . 6 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)))
80		df-fn 6495	. . . . . . . 8 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → Fun 𝐺)
83	81, 82	anim12i 619	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84	83	3adant3 1138	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85		ineq12 4151	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴 ∖ 𝐵)))
86	85, 7	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
87	86	ad2ant2l 752	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88	87	3adant3 1138	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89		fvun 6924	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
90	84, 88, 89	syl2anc 590	. . . . . . . . . . 11 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
91	90	eleq1d 2825	. . . . . . . . . 10 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
92	91	ralbidv 3163	. . . . . . . . 9 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
93	92	3exp 1125	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
94	80, 93	sylbi 218	. . . . . . 7 ⊢ (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
95	94	com12 32	. . . . . 6 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
96	79, 95	sylbi 218	. . . . 5 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
97	3, 4, 96	syl2imc 41	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
98	97	3imp 1116	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
99	78, 98	mpbird 258	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶)
100		elixp2 8846	. 2 ⊢ ((𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶 ↔ ((𝐹 ∪ 𝐺) ∈ V ∧ (𝐹 ∪ 𝐺) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶))
101	2, 18, 99, 100	syl3anbrc 1350	1 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3054 Vcvv 3432 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4268 dom cdm 5625 Fun wfun 6486 Fn wfn 6487 ‘cfv 6492 Xcixp 8842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pr 5369 ax-un 7685

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-br 5080 df-opab 5142 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6448 df-fun 6494 df-fn 6495 df-fv 6500 df-ixp 8843

This theorem is referenced by: ptuncnv 23797 ptunhmeo 23798

W3C validator