Theorem canthp1lem1

Description: Lemma for canthp1 . (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	canthp1lem1	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1sdom2	⊢ 1o ≺ 2o
2		djuxpdom	⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 2o ) → ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) )
3	1 2	mpan2	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) )
4		sdom0	⊢ ¬ 1o ≺ ∅
5		breq2	⊢ ( 𝐴 = ∅ → ( 1o ≺ 𝐴 ↔ 1o ≺ ∅ ) )
6	4 5	mtbiri	⊢ ( 𝐴 = ∅ → ¬ 1o ≺ 𝐴 )
7	6	con2i	⊢ ( 1o ≺ 𝐴 → ¬ 𝐴 = ∅ )
8		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
9	7 8	sylib	⊢ ( 1o ≺ 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐴 )
10		relsdom	⊢ Rel ≺
11	10	brrelex2i	⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
12	11	adantr	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ V )
13		enrefg	⊢ ( 𝐴 ∈ V → 𝐴 ≈ 𝐴 )
14	12 13	syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≈ 𝐴 )
15		df2o2	⊢ 2o = { ∅ , { ∅ } }
16		pwpw0	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }
17	15 16	eqtr4i	⊢ 2o = 𝒫 { ∅ }
18		0ex	⊢ ∅ ∈ V
19		vex	⊢ 𝑥 ∈ V
20		en2sn	⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } )
21	18 19 20	mp2an	⊢ { ∅ } ≈ { 𝑥 }
22		pwen	⊢ ( { ∅ } ≈ { 𝑥 } → 𝒫 { ∅ } ≈ 𝒫 { 𝑥 } )
23	21 22	ax-mp	⊢ 𝒫 { ∅ } ≈ 𝒫 { 𝑥 }
24	17 23	eqbrtri	⊢ 2o ≈ 𝒫 { 𝑥 }
25		xpen	⊢ ( ( 𝐴 ≈ 𝐴 ∧ 2o ≈ 𝒫 { 𝑥 } ) → ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) )
26	14 24 25	sylancl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) )
27		snex	⊢ { 𝑥 } ∈ V
28	27	pwex	⊢ 𝒫 { 𝑥 } ∈ V
29		uncom	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) )
30		simpr	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
31	30	snssd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ⊆ 𝐴 )
32		undif	⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 )
33	31 32	sylib	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = 𝐴 )
34	29 33	eqtrid	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 )
35	12	difexd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ V )
36		canth2g	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∈ V → ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
37		domunsn	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
38	35 36 37	3syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
39	34 38	eqbrtrrd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
40		xpdom1g	⊢ ( ( 𝒫 { 𝑥 } ∈ V ∧ 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
41	28 39 40	sylancr	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
42		endomtr	⊢ ( ( ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ∧ ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
43	26 41 42	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
44		pwdjuen	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
45	35 27 44	sylancl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
46	45	ensymd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
47		domentr	⊢ ( ( ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ∧ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
48	43 46 47	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
49	27	a1i	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ V )
50		disjdifr	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
51	50	a1i	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
52		endjudisj	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ∧ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
53	35 49 51 52	syl3anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
54	53 34	breqtrd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 )
55		pwen	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
56	54 55	syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
57		domentr	⊢ ( ( ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ∧ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
58	48 56 57	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
59	9 58	exlimddv	⊢ ( 1o ≺ 𝐴 → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
60		domtr	⊢ ( ( ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ∧ ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
61	3 59 60	syl2anc	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )