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	syl5eq	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 )
35		difexg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ { 𝑥 } ) ∈ V )
36	12 35	syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ V )
37		canth2g	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∈ V → ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
38		domunsn	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ≺ 𝒫 ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
39	36 37 38	3syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
40	34 39	eqbrtrrd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) )
41		xpdom1g	⊢ ( ( 𝒫 { 𝑥 } ∈ V ∧ 𝐴 ≼ 𝒫 ( 𝐴 ∖ { 𝑥 } ) ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
42	28 40 41	sylancr	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
43		endomtr	⊢ ( ( ( 𝐴 × 2o ) ≈ ( 𝐴 × 𝒫 { 𝑥 } ) ∧ ( 𝐴 × 𝒫 { 𝑥 } ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
44	26 42 43	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
45		pwdjuen	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
46	36 27 45	sylancl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) )
47	46	ensymd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
48		domentr	⊢ ( ( ( 𝐴 × 2o ) ≼ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ∧ ( 𝒫 ( 𝐴 ∖ { 𝑥 } ) × 𝒫 { 𝑥 } ) ≈ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
49	44 47 48	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) )
50	27	a1i	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ V )
51		incom	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) )
52		disjdif	⊢ ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅
53	51 52	eqtri	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
54	53	a1i	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
55		endjudisj	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ∈ V ∧ { 𝑥 } ∈ V ∧ ( ( 𝐴 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
56	36 50 54 55	syl3anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
57	56 34	breqtrd	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 )
58		pwen	⊢ ( ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝐴 → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
59	57 58	syl	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 )
60		domentr	⊢ ( ( ( 𝐴 × 2o ) ≼ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ∧ 𝒫 ( ( 𝐴 ∖ { 𝑥 } ) ⊔ { 𝑥 } ) ≈ 𝒫 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
61	49 59 60	syl2anc	⊢ ( ( 1o ≺ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
62	9 61	exlimddv	⊢ ( 1o ≺ 𝐴 → ( 𝐴 × 2o ) ≼ 𝒫 𝐴 )
63		domtr	⊢ ( ( ( 𝐴 ⊔ 2o ) ≼ ( 𝐴 × 2o ) ∧ ( 𝐴 × 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
64	3 62 63	syl2anc	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )