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		vsnex	⊢ { 𝑧 } ∈ V
16	15	0dom	⊢ ∅ ≼ { 𝑧 }
17	14 16	eqbrtrdi	⊢ ( ¬ 𝐶 ∈ V → { 𝐶 } ≼ { 𝑧 } )
18	12 17	pm2.61i	⊢ { 𝐶 } ≼ { 𝑧 }
19		disjdifr	⊢ ( ( 𝐵 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅
20		undom	⊢ ( ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) ∧ { 𝐶 } ≼ { 𝑧 } ) ∧ ( ( 𝐵 ∖ { 𝑧 } ) ∩ { 𝑧 } ) = ∅ ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
21	19 20	mpan2	⊢ ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑧 } ) ∧ { 𝐶 } ≼ { 𝑧 } ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
22	8 18 21	sylancl	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∪ { 𝐶 } ) ≼ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
23		uncom	⊢ ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) )
24		simpr	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
25	24	snssd	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → { 𝑧 } ⊆ 𝐵 )
26		undif	⊢ ( { 𝑧 } ⊆ 𝐵 ↔ ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) ) = 𝐵 )
27	25 26	sylib	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( { 𝑧 } ∪ ( 𝐵 ∖ { 𝑧 } ) ) = 𝐵 )
28	23 27	eqtrid	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐵 ∖ { 𝑧 } ) ∪ { 𝑧 } ) = 𝐵 )
29	22 28	breqtrd	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∪ { 𝐶 } ) ≼ 𝐵 )
30	6 29	exlimddv	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐴 ∪ { 𝐶 } ) ≼ 𝐵 )

Metamath Proof Explorer

Theorem domunsn

Proof