Theorem domunsn

Description: Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	domunsn	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐴 ∪ { 𝐶 } ) ≼ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sdom0	⊢ ¬ 𝐴 ≺ ∅
2		breq2	⊢ ( 𝐵 = ∅ → ( 𝐴 ≺ 𝐵 ↔ 𝐴 ≺ ∅ ) )
3	1 2	mtbiri	⊢ ( 𝐵 = ∅ → ¬ 𝐴 ≺ 𝐵 )
4	3	con2i	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐵 = ∅ )
5		neq0	⊢ ( ¬ 𝐵 = ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐵 )
6	4 5	sylib	⊢ ( 𝐴 ≺ 𝐵 → ∃ 𝑧 𝑧 ∈ 𝐵 )
7		domdifsn	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) )
8	7	adantr	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) )
9		en2sn	⊢ ( ( 𝐶 ∈ V ∧ 𝑧 ∈ V ) → { 𝐶 } ≈ { 𝑧 } )
10	9	elvd	⊢ ( 𝐶 ∈ V → { 𝐶 } ≈ { 𝑧 } )
11		endom	⊢ ( { 𝐶 } ≈ { 𝑧 } → { 𝐶 } ≼ { 𝑧 } )
12	10 11	syl	⊢ ( 𝐶 ∈ V → { 𝐶 } ≼ { 𝑧 } )
13		snprc	⊢ ( ¬ 𝐶 ∈ V ↔ { 𝐶 } = ∅ )
14	13	biimpi	⊢ ( ¬ 𝐶 ∈ V → { 𝐶 } = ∅ )
15		snex	⊢ { 𝑧 } ∈ V
16	15	0dom	⊢ ∅ ≼ { 𝑧 }
17	14 16	eqbrtrdi	⊢ ( ¬ 𝐶 ∈ V → { 𝐶 } ≼ { 𝑧 } )
18	12 17	pm2.61i	⊢ { 𝐶 } ≼ { 𝑧 }
19		incom	⊢ ( ( 𝐵 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ( { 𝑧 } ∩ ( 𝐵 ∖ { 𝑧 } ) )
20		disjdif	⊢ ( { 𝑧 } ∩ ( 𝐵 ∖ { 𝑧 } ) ) = ∅
21	19 20	eqtri	⊢ ( ( 𝐵 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅
22		undom	⊢ ( ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) ∧ { 𝐶 } ≼ { 𝑧 } ) ∧ ( ( 𝐵 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
23	21 22	mpan2	⊢ ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) ∧ { 𝐶 } ≼ { 𝑧 } ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
24	8 18 23	sylancl	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
25		uncom	⊢ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) )
26		simpr	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
27	26	snssd	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → { 𝑧 } ⊆ 𝐵 )
28		undif	⊢ ( { 𝑧 } ⊆ 𝐵 ↔ ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) ) = 𝐵 )
29	27 28	sylib	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) ) = 𝐵 )
30	25 29	syl5eq	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝐵 )
31	24 30	breqtrd	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∪ { 𝐶 } ) ≼ 𝐵 )
32	6 31	exlimddv	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐴 ∪ { 𝐶 } ) ≼ 𝐵 )