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 8974

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 7763	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → (𝐹 ∪ 𝐺) ∈ V)
2	1	3adant3 1133	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ V)
3		ixpfn 8943	. . . 4 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → 𝐺 Fn (𝐴 ∖ 𝐵))
4		ixpfn 8943	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → 𝐹 Fn 𝐵)
5		3simpa 1149	. . . . . . . 8 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵))
6	5	ancomd 461	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)))
7		disjdif 4472	. . . . . . 7 ⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅
8		fnun 6682	. . . . . . 7 ⊢ (((𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)) ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
9	6, 7, 8	sylancl 586	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))
10		undif 4482	. . . . . . . . . 10 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
11	10	biimpi 216	. . . . . . . . 9 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴)
12	11	eqcomd 2743	. . . . . . . 8 ⊢ (𝐵 ⊆ 𝐴 → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
13	12	3ad2ant3 1136	. . . . . . 7 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
14	13	fneq2d 6662	. . . . . 6 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺) Fn 𝐴 ↔ (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))))
15	9, 14	mpbird 257	. . . . 5 ⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
16	15	3exp 1120	. . . 4 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
17	3, 4, 16	syl2imc 41	. . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴)))
18	17	3imp 1111	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴)
19		elixp2 8941	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶))
20	19	simp3bi 1148	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶)
21		fndm 6671	. . . . . . . . . . . . . 14 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → dom 𝐺 = (𝐴 ∖ 𝐵))
22		elndif 4133	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
23		eleq2 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 𝑥 ∈ dom 𝐺))
24	23	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
25	24	eqcoms 2745	. . . . . . . . . . . . . . 15 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺))
26		ndmfv 6941	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) = ∅)
27	25, 26	biimtrdi 253	. . . . . . . . . . . . . 14 ⊢ (dom 𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐺‘𝑥) = ∅))
28	21, 22, 27	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐵 → (𝐺‘𝑥) = ∅))
29	28	ralrimiv 3145	. . . . . . . . . . . 12 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅)
30		uneq2 4162	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅))
31		un0 4394	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)
32		eqtr 2760	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥))
33		eleq1 2829	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
34	33	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
35	34	eqcoms 2745	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
36	32, 35	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
37	30, 31, 36	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
38	37	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ 𝐶 → ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
39	38	ral2imi 3085	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
40	20, 29, 39	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
41	3, 40	syl 17	. . . . . . . . . 10 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
42	41	impcom 407	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
43		elixp2 8941	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 ∖ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶))
44	43	simp3bi 1148	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶)
45		fndm 6671	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵)
46		eldifn 4132	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
47		eleq2 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = dom 𝐹 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹))
48	47	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹))
49		ndmfv 6941	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ∅)
50	48, 49	biimtrdi 253	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
51	50	eqcoms 2745	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 = 𝐵 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅))
52	45, 46, 51	syl2im 40	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐹‘𝑥) = ∅))
53	52	ralrimiv 3145	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅)
54		uneq1 4161	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)))
55		uncom 4158	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)
56		eqtr 2760	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅))
57		un0 4394	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)
58		eqtr 2760	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥))
59		eleq1 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
60	59	biimpd 229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
61	60	eqcoms 2745	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
62	58, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
63	56, 57, 62	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
64	54, 55, 63	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = ∅ → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
65	64	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
66	65	ral2imi 3085	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
67	44, 53, 66	syl2imc 41	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐵 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
68	4, 67	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
69	68	imp 406	. . . . . . . . 9 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
70		ralunb 4197	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ (∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
71	42, 69, 70	sylanbrc 583	. . . . . . . 8 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
72	71	ex 412	. . . . . . 7 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
73		raleq 3323	. . . . . . . 8 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
74	73	imbi2d 340	. . . . . . 7 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → ((𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) ↔ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
75	72, 74	imbitrrid 246	. . . . . 6 ⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
76	75	eqcoms 2745	. . . . 5 ⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
77	10, 76	sylbi 217	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))
78	77	3imp231 1113	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)
79		df-fn 6564	. . . . . 6 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)))
80		df-fn 6564	. . . . . . . 8 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
81		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹)
82		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → Fun 𝐺)
83	81, 82	anim12i 613	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (Fun 𝐹 ∧ Fun 𝐺))
84	83	3adant3 1133	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (Fun 𝐹 ∧ Fun 𝐺))
85		ineq12 4215	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴 ∖ 𝐵)))
86	85, 7	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
87	86	ad2ant2l 746	. . . . . . . . . . . . 13 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅)
88	87	3adant3 1133	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)
89		fvun 6999	. . . . . . . . . . . 12 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
90	84, 88, 89	syl2anc 584	. . . . . . . . . . 11 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)))
91	90	eleq1d 2826	. . . . . . . . . 10 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
92	91	ralbidv 3178	. . . . . . . . 9 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
93	92	3exp 1120	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
94	80, 93	sylbi 217	. . . . . . 7 ⊢ (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
95	94	com12 32	. . . . . 6 ⊢ ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
96	79, 95	sylbi 217	. . . . 5 ⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
97	3, 4, 96	syl2imc 41	. . . 4 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))))
98	97	3imp 1111	. . 3 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))
99	78, 98	mpbird 257	. 2 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶)
100		elixp2 8941	. 2 ⊢ ((𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶 ↔ ((𝐹 ∪ 𝐺) ∈ V ∧ (𝐹 ∪ 𝐺) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶))
101	2, 18, 99, 100	syl3anbrc 1344	1 ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 dom cdm 5685 Fun wfun 6555 Fn wfn 6556 ‘cfv 6561 Xcixp 8937

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-fv 6569 df-ixp 8938

This theorem is referenced by: ptuncnv 23815 ptunhmeo 23816

W3C validator