Theorem domunsncan 8616

Description: A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)

Hypotheses

Ref	Expression
domunsncan.a	⊢ 𝐴 ∈ V
domunsncan.b	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
domunsncan	⊢ ((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) ↔ 𝑋 ≼ 𝑌))

Proof of Theorem domunsncan

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssun2 4148	. . . 4 ⊢ 𝑌 ⊆ ({𝐵} ∪ 𝑌)
2		reldom 8514	. . . . . 6 ⊢ Rel ≼
3	2	brrelex2i 5608	. . . . 5 ⊢ (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → ({𝐵} ∪ 𝑌) ∈ V)
4	3	adantl 484	. . . 4 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → ({𝐵} ∪ 𝑌) ∈ V)
5		ssexg 5226	. . . 4 ⊢ ((𝑌 ⊆ ({𝐵} ∪ 𝑌) ∧ ({𝐵} ∪ 𝑌) ∈ V) → 𝑌 ∈ V)
6	1, 4, 5	sylancr 589	. . 3 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → 𝑌 ∈ V)
7		brdomi 8519	. . . . 5 ⊢ (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → ∃𝑓 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))
8		vex 3497	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
9	8	resex 5898	. . . . . . . . . 10 ⊢ (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∈ V
10		simprr 771	. . . . . . . . . . 11 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))
11		difss 4107	. . . . . . . . . . 11 ⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) ⊆ ({𝐴} ∪ 𝑋)
12		f1ores 6628	. . . . . . . . . . 11 ⊢ ((𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) ∧ (({𝐴} ∪ 𝑋) ∖ {𝐴}) ⊆ ({𝐴} ∪ 𝑋)) → (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})))
13	10, 11, 12	sylancl 588	. . . . . . . . . 10 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})))
14		f1oen3g 8524	. . . . . . . . . 10 ⊢ (((𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∈ V ∧ (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})))
15	9, 13, 14	sylancr 589	. . . . . . . . 9 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})))
16		df-f1 6359	. . . . . . . . . . . 12 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) ↔ (𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) ∧ Fun ◡𝑓))
17		imadif 6437	. . . . . . . . . . . 12 ⊢ (Fun ◡𝑓 → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})))
18	16, 17	simplbiim 507	. . . . . . . . . . 11 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})))
19	18	ad2antll 727	. . . . . . . . . 10 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})))
20		snex 5331	. . . . . . . . . . . . . 14 ⊢ {𝐵} ∈ V
21		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑌 ∈ V)
22		unexg 7471	. . . . . . . . . . . . . 14 ⊢ (({𝐵} ∈ V ∧ 𝑌 ∈ V) → ({𝐵} ∪ 𝑌) ∈ V)
23	20, 21, 22	sylancr 589	. . . . . . . . . . . . 13 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ({𝐵} ∪ 𝑌) ∈ V)
24		difexg 5230	. . . . . . . . . . . . 13 ⊢ (({𝐵} ∪ 𝑌) ∈ V → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V)
25	23, 24	syl 17	. . . . . . . . . . . 12 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V)
26		f1f 6574	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌))
27		fimass 6554	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌))
28	26, 27	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌))
29	28	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌))
30	29	ssdifd 4116	. . . . . . . . . . . . 13 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ (𝑓 “ {𝐴})))
31		f1fn 6575	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑓 Fn ({𝐴} ∪ 𝑋))
32	31	ad2antll 727	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑓 Fn ({𝐴} ∪ 𝑋))
33		domunsncan.a	. . . . . . . . . . . . . . . . 17 ⊢ 𝐴 ∈ V
34	33	snid 4600	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ∈ {𝐴}
35		elun1 4151	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ ({𝐴} ∪ 𝑋))
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ∈ ({𝐴} ∪ 𝑋)
37		fnsnfv 6742	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ({𝐴} ∪ 𝑋) ∧ 𝐴 ∈ ({𝐴} ∪ 𝑋)) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴}))
38	32, 36, 37	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴}))
39	38	difeq2d 4098	. . . . . . . . . . . . 13 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) = (({𝐵} ∪ 𝑌) ∖ (𝑓 “ {𝐴})))
40	30, 39	sseqtrrd 4007	. . . . . . . . . . . 12 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}))
41		ssdomg 8554	. . . . . . . . . . . 12 ⊢ ((({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V → (((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)})))
42	25, 40, 41	sylc 65	. . . . . . . . . . 11 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}))
43		ffvelrn 6848	. . . . . . . . . . . . . 14 ⊢ ((𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) ∧ 𝐴 ∈ ({𝐴} ∪ 𝑋)) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌))
44	26, 36, 43	sylancl 588	. . . . . . . . . . . . 13 ⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌))
45	44	ad2antll 727	. . . . . . . . . . . 12 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌))
46		domunsncan.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
47	46	snid 4600	. . . . . . . . . . . . 13 ⊢ 𝐵 ∈ {𝐵}
48		elun1 4151	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ ({𝐵} ∪ 𝑌))
49	47, 48	mp1i 13	. . . . . . . . . . . 12 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝐵 ∈ ({𝐵} ∪ 𝑌))
50		difsnen 8598	. . . . . . . . . . . 12 ⊢ ((({𝐵} ∪ 𝑌) ∈ V ∧ (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌) ∧ 𝐵 ∈ ({𝐵} ∪ 𝑌)) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
51	23, 45, 49, 50	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
52		domentr 8567	. . . . . . . . . . 11 ⊢ ((((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∧ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵})) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
53	42, 51, 52	syl2anc 586	. . . . . . . . . 10 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
54	19, 53	eqbrtrd 5087	. . . . . . . . 9 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
55		endomtr 8566	. . . . . . . . 9 ⊢ (((({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∧ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
56	15, 54, 55	syl2anc 586	. . . . . . . 8 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵}))
57		uncom 4128	. . . . . . . . . . . 12 ⊢ ({𝐴} ∪ 𝑋) = (𝑋 ∪ {𝐴})
58	57	difeq1i 4094	. . . . . . . . . . 11 ⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) = ((𝑋 ∪ {𝐴}) ∖ {𝐴})
59		difun2 4428	. . . . . . . . . . 11 ⊢ ((𝑋 ∪ {𝐴}) ∖ {𝐴}) = (𝑋 ∖ {𝐴})
60	58, 59	eqtri 2844	. . . . . . . . . 10 ⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) = (𝑋 ∖ {𝐴})
61		difsn 4730	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ 𝑋 → (𝑋 ∖ {𝐴}) = 𝑋)
62	60, 61	syl5eq 2868	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ 𝑋 → (({𝐴} ∪ 𝑋) ∖ {𝐴}) = 𝑋)
63	62	ad2antrr 724	. . . . . . . 8 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) = 𝑋)
64		uncom 4128	. . . . . . . . . . . 12 ⊢ ({𝐵} ∪ 𝑌) = (𝑌 ∪ {𝐵})
65	64	difeq1i 4094	. . . . . . . . . . 11 ⊢ (({𝐵} ∪ 𝑌) ∖ {𝐵}) = ((𝑌 ∪ {𝐵}) ∖ {𝐵})
66		difun2 4428	. . . . . . . . . . 11 ⊢ ((𝑌 ∪ {𝐵}) ∖ {𝐵}) = (𝑌 ∖ {𝐵})
67	65, 66	eqtri 2844	. . . . . . . . . 10 ⊢ (({𝐵} ∪ 𝑌) ∖ {𝐵}) = (𝑌 ∖ {𝐵})
68		difsn 4730	. . . . . . . . . 10 ⊢ (¬ 𝐵 ∈ 𝑌 → (𝑌 ∖ {𝐵}) = 𝑌)
69	67, 68	syl5eq 2868	. . . . . . . . 9 ⊢ (¬ 𝐵 ∈ 𝑌 → (({𝐵} ∪ 𝑌) ∖ {𝐵}) = 𝑌)
70	69	ad2antlr 725	. . . . . . . 8 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {𝐵}) = 𝑌)
71	56, 63, 70	3brtr3d 5096	. . . . . . 7 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑋 ≼ 𝑌)
72	71	expr 459	. . . . . 6 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌))
73	72	exlimdv 1930	. . . . 5 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (∃𝑓 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌))
74	7, 73	syl5 34	. . . 4 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌))
75	74	impancom 454	. . 3 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → (𝑌 ∈ V → 𝑋 ≼ 𝑌))
76	6, 75	mpd 15	. 2 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → 𝑋 ≼ 𝑌)
77		en2sn 8592	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴} ≈ {𝐵})
78	33, 46, 77	mp2an 690	. . . 4 ⊢ {𝐴} ≈ {𝐵}
79		endom 8535	. . . 4 ⊢ ({𝐴} ≈ {𝐵} → {𝐴} ≼ {𝐵})
80	78, 79	mp1i 13	. . 3 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → {𝐴} ≼ {𝐵})
81		simpr 487	. . 3 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → 𝑋 ≼ 𝑌)
82		incom 4177	. . . . 5 ⊢ ({𝐵} ∩ 𝑌) = (𝑌 ∩ {𝐵})
83		disjsn 4646	. . . . . 6 ⊢ ((𝑌 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝑌)
84	83	biimpri 230	. . . . 5 ⊢ (¬ 𝐵 ∈ 𝑌 → (𝑌 ∩ {𝐵}) = ∅)
85	82, 84	syl5eq 2868	. . . 4 ⊢ (¬ 𝐵 ∈ 𝑌 → ({𝐵} ∩ 𝑌) = ∅)
86	85	ad2antlr 725	. . 3 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → ({𝐵} ∩ 𝑌) = ∅)
87		undom 8604	. . 3 ⊢ ((({𝐴} ≼ {𝐵} ∧ 𝑋 ≼ 𝑌) ∧ ({𝐵} ∩ 𝑌) = ∅) → ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌))
88	80, 81, 86, 87	syl21anc 835	. 2 ⊢ (((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌))
89	76, 88	impbida 799	1 ⊢ ((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) ↔ 𝑋 ≼ 𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110  Vcvv 3494   ∖ cdif 3932   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  {csn 4566   class class class wbr 5065  ^◡ccnv 5553   ↾ cres 5556   “ cima 5557  Fun wfun 6348   Fn wfn 6349  ⟶wf 6350  –1-1→wf1 6351  –1-1-onto→wf1o 6353  ‘cfv 6354   ≈ cen 8505   ≼ cdom 8506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-1o 8101  df-er 8288  df-en 8509  df-dom 8510

This theorem is referenced by:  domunfican  8790