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 8912

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 7722	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → (𝐹 ∪ 𝐺) ∈ V)
2	1	3adant3 1144	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ V)
3		ixpfn 8881	. . . 4 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → 𝐺 Fn (𝐴 ∖ 𝐵))
4		ixpfn 8881	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → 𝐹 Fn 𝐵)
5		3simpa 1160	. . . . . . . 8 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵))
6	5	ancomd 465	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)))
7		disjdif 4425	. . . . . . 7 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅
8		fnun 6631	. . . . . . 7 ⊢ (((𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)) ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
9	6, 7, 8	sylancl 595	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
10		undif 4435	. . . . . . . . . 10 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
11	10	biimpi 218	. . . . . . . . 9 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
12	11	eqcomd 2767	. . . . . . . 8 ⊢ (𝐵 ⊆ 𝐴 → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
13	12	3ad2ant3 1147	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
14	13	fneq2d 6611	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺) Fn 𝐴 ↔ (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))))
15	9, 14	mpbird 259	. . . . 5 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
16	15	3exp 1131	. . . 4 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
17	3, 4, 16	syl2imc 41	. . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
18	17	3imp 1122	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
19		elixp2 8879	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶))
20	19	simp3bi 1159	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶)
21		fndm 6620	. . . . . . . . . . . . . 14 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → dom 𝐺 = (𝐴 ∖ 𝐵))
22		elndif 4086	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
23		eleq2 2850	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 𝑥 ∈ dom 𝐺))
24	23	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
25	24	eqcoms 2769	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26		ndmfv 6895	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) = ∅)
27	25, 26	biimtrdi 255	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐺‘𝑥) = ∅))
28	21, 22, 27	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐵 → (𝐺‘𝑥) = ∅))
29	28	ralrimiv 3152	. . . . . . . . . . . 12 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅)
30		uneq2 4115	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅))
31		un0 4347	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)
32		eqtr 2781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥))
33		eleq1 2849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
34	33	biimpd 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
35	34	eqcoms 2769	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
36	32, 35	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
37	30, 31, 36	sylancl 595	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
38	37	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ 𝐶 → ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
39	38	ral2imi 3100	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
40	20, 29, 39	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
41	3, 40	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
42	41	impcom 411	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
43		elixp2 8879	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 ∖ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶))
44	43	simp3bi 1159	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶)
45		fndm 6620	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46		eldifn 4085	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
47		eleq2 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = dom 𝐹 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹))
48	47	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49		ndmfv 6895	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ∅)
50	48, 49	biimtrdi 255	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
51	50	eqcoms 2769	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 = 𝐵 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
52	45, 46, 51	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐹‘𝑥) = ∅))
53	52	ralrimiv 3152	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅)
54		uneq1 4114	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)))
55		uncom 4111	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)
56		eqtr 2781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅))
57		un0 4347	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)
58		eqtr 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥))
59		eleq1 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
60	59	biimpd 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
61	60	eqcoms 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
63	56, 57, 62	sylancl 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
64	54, 55, 63	sylancl 595	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
65	64	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
66	65	ral2imi 3100	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
67	44, 53, 66	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐵 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
68	4, 67	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
69	68	imp 410	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
70		ralunb 4149	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ (∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
71	42, 69, 70	sylanbrc 592	. . . . . . . 8 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
72	71	ex 416	. . . . . . 7 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
73		raleq 3316	. . . . . . . 8 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
74	73	imbi2d 342	. . . . . . 7 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → ((𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) ↔ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
75	72, 74	imbitrrid 248	. . . . . 6 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
76	75	eqcoms 2769	. . . . 5 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
77	10, 76	sylbi 219	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
78	77	3imp231 1124	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
79		df-fn 6520	. . . . . 6 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)))
80		df-fn 6520	. . . . . . . 8 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → Fun 𝐺)
83	81, 82	anim12i 622	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84	83	3adant3 1144	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85		ineq12 4167	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴 ∖ 𝐵)))
86	85, 7	eqtrdi 2812	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
87	86	ad2ant2l 756	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88	87	3adant3 1144	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89		fvun 6953	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
90	84, 88, 89	syl2anc 593	. . . . . . . . . . 11 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
91	90	eleq1d 2846	. . . . . . . . . 10 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
92	91	ralbidv 3184	. . . . . . . . 9 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
93	92	3exp 1131	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
94	80, 93	sylbi 219	. . . . . . 7 ⊢ (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
95	94	com12 32	. . . . . 6 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
96	79, 95	sylbi 219	. . . . 5 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
97	3, 4, 96	syl2imc 41	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
98	97	3imp 1122	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
99	78, 98	mpbird 259	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶)
100		elixp2 8879	. 2 ⊢ ((𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶 ↔ ((𝐹 ∪ 𝐺) ∈ V ∧ (𝐹 ∪ 𝐺) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶))
101	2, 18, 99, 100	syl3anbrc 1356	1 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 Vcvv 3453 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 dom cdm 5645 Fun wfun 6511 Fn wfn 6512 ‘cfv 6517 Xcixp 8875

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pr 5389 ax-un 7714

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-id 5540 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-iota 6473 df-fun 6519 df-fn 6520 df-fv 6525 df-ixp 8876

This theorem is referenced by: ptuncnv 23847 ptunhmeo 23848

W3C validator