canthp1lem2

	Ref	Expression
Hypotheses	canthp1lem2.1	⊢ ( 𝜑 → 1_o ≺ 𝐴 )
	canthp1lem2.2	⊢ ( 𝜑 → 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) )
	canthp1lem2.3	⊢ ( 𝜑 → 𝐺 : ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
	canthp1lem2.4	⊢ 𝐻 = ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) )
	canthp1lem2.5	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐻 ‘ ( ^◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
	canthp1lem2.6	⊢ 𝐵 = ∪ dom 𝑊
Assertion	canthp1lem2	⊢ ¬ 𝜑

Proof

Step	Hyp	Ref	Expression
1		canthp1lem2.1	⊢ ( 𝜑 → 1_o ≺ 𝐴 )
2		canthp1lem2.2	⊢ ( 𝜑 → 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) )
3		canthp1lem2.3	⊢ ( 𝜑 → 𝐺 : ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 )
4		canthp1lem2.4	⊢ 𝐻 = ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) )
5		canthp1lem2.5	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐻 ‘ ( ^◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
6		canthp1lem2.6	⊢ 𝐵 = ∪ dom 𝑊
7		relsdom	⊢ Rel ≺
8	7	brrelex2i	⊢ ( 1_o ≺ 𝐴 → 𝐴 ∈ V )
9	1 8	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
10	9	pwexd	⊢ ( 𝜑 → 𝒫 𝐴 ∈ V )
11		f1oeng	⊢ ( ( 𝒫 𝐴 ∈ V ∧ 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) ) → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1_o ) )
12	10 2 11	syl2anc	⊢ ( 𝜑 → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1_o ) )
13	12	ensymd	⊢ ( 𝜑 → ( 𝐴 ⊔ 1_o ) ≈ 𝒫 𝐴 )
14		canth2g	⊢ ( 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴 )
15	9 14	syl	⊢ ( 𝜑 → 𝐴 ≺ 𝒫 𝐴 )
16		sdomen2	⊢ ( 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1_o ) → ( 𝐴 ≺ 𝒫 𝐴 ↔ 𝐴 ≺ ( 𝐴 ⊔ 1_o ) ) )
17	12 16	syl	⊢ ( 𝜑 → ( 𝐴 ≺ 𝒫 𝐴 ↔ 𝐴 ≺ ( 𝐴 ⊔ 1_o ) ) )
18	15 17	mpbid	⊢ ( 𝜑 → 𝐴 ≺ ( 𝐴 ⊔ 1_o ) )
19		sdomnen	⊢ ( 𝐴 ≺ ( 𝐴 ⊔ 1_o ) → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1_o ) )
20	18 19	syl	⊢ ( 𝜑 → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1_o ) )
21		omelon	⊢ ω ∈ On
22		onenon	⊢ ( ω ∈ On → ω ∈ dom card )
23	21 22	ax-mp	⊢ ω ∈ dom card
24		dff1o3	⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) ↔ ( 𝐹 : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ∧ Fun ^◡ 𝐹 ) )
25	24	simprbi	⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) → Fun ^◡ 𝐹 )
26	2 25	syl	⊢ ( 𝜑 → Fun ^◡ 𝐹 )
27		f1ofo	⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) → 𝐹 : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) )
28	2 27	syl	⊢ ( 𝜑 → 𝐹 : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) )
29		f1ofn	⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ ( 𝐴 ⊔ 1_o ) → 𝐹 Fn 𝒫 𝐴 )
30		fnresdm	⊢ ( 𝐹 Fn 𝒫 𝐴 → ( 𝐹 ↾ 𝒫 𝐴 ) = 𝐹 )
31		foeq1	⊢ ( ( 𝐹 ↾ 𝒫 𝐴 ) = 𝐹 → ( ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ↔ 𝐹 : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ) )
32	2 29 30 31	4syl	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ↔ 𝐹 : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ) )
33	28 32	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) )
34		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
35		f1osng	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } )
36	9 34 35	sylancl	⊢ ( 𝜑 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } )
37	2 29	syl	⊢ ( 𝜑 → 𝐹 Fn 𝒫 𝐴 )
38		pwidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
39	9 38	syl	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐴 )
40		fnressn	⊢ ( ( 𝐹 Fn 𝒫 𝐴 ∧ 𝐴 ∈ 𝒫 𝐴 ) → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
41	37 39 40	syl2anc	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
42	41	f1oeq1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } ) )
43	36 42	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } )
44		f1ofo	⊢ ( ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹 ‘ 𝐴 ) } → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹 ‘ 𝐴 ) } )
45	43 44	syl	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹 ‘ 𝐴 ) } )
46		resdif	⊢ ( ( Fun ^◡ 𝐹 ∧ ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴 –onto→ ( 𝐴 ⊔ 1_o ) ∧ ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹 ‘ 𝐴 ) } ) → ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) )
47	26 33 45 46	syl3anc	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) )
48		f1oco	⊢ ( ( 𝐺 : ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) –1-1-onto→ 𝐴 ∧ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1_o ) ∖ { ( 𝐹 ‘ 𝐴 ) } ) ) → ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 )
49	3 47 48	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 )
50		resco	⊢ ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) = ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) )
51		f1oeq1	⊢ ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) = ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 ↔ ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 ) )
52	50 51	ax-mp	⊢ ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 ↔ ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 )
53	49 52	sylibr	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 )
54		f1of	⊢ ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) ⟶ 𝐴 )
55	53 54	syl	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) ⟶ 𝐴 )
56		0elpw	⊢ ∅ ∈ 𝒫 𝐴
57	56	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ∈ 𝒫 𝐴 )
58		sdom0	⊢ ¬ 1_o ≺ ∅
59		breq2	⊢ ( ∅ = 𝐴 → ( 1_o ≺ ∅ ↔ 1_o ≺ 𝐴 ) )
60	58 59	mtbii	⊢ ( ∅ = 𝐴 → ¬ 1_o ≺ 𝐴 )
61	60	necon2ai	⊢ ( 1_o ≺ 𝐴 → ∅ ≠ 𝐴 )
62	1 61	syl	⊢ ( 𝜑 → ∅ ≠ 𝐴 )
63	62	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ≠ 𝐴 )
64		eldifsn	⊢ ( ∅ ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( ∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴 ) )
65	57 63 64	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
66		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝒫 𝐴 )
67		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → ¬ 𝑥 = 𝐴 )
68	67	neqned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐴 )
69		eldifsn	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ≠ 𝐴 ) )
70	66 68 69	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
71	65 70	ifclda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ) → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
72	71	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) : 𝒫 𝐴 ⟶ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
73	55 72	fcod	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) : 𝒫 𝐴 ⟶ 𝐴 )
74	72	frnd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ⊆ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
75		cores	⊢ ( ran ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ⊆ ( 𝒫 𝐴 ∖ { 𝐴 } ) → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) )
76	74 75	syl	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) )
77	76 4	eqtr4di	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = 𝐻 )
78	77	feq1d	⊢ ( 𝜑 → ( ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) : 𝒫 𝐴 ⟶ 𝐴 ↔ 𝐻 : 𝒫 𝐴 ⟶ 𝐴 ) )
79	73 78	mpbid	⊢ ( 𝜑 → 𝐻 : 𝒫 𝐴 ⟶ 𝐴 )
80		inss1	⊢ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴
81	80	a1i	⊢ ( 𝜑 → ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴 )
82		eqid	⊢ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } )
83	5 6 82	canth4	⊢ ( ( 𝐴 ∈ V ∧ 𝐻 : 𝒫 𝐴 ⟶ 𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊊ 𝐵 ∧ ( 𝐻 ‘ 𝐵 ) = ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) )
84	9 79 81 83	syl3anc	⊢ ( 𝜑 → ( 𝐵 ⊆ 𝐴 ∧ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊊ 𝐵 ∧ ( 𝐻 ‘ 𝐵 ) = ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) )
85	84	simp1d	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
86	84	simp2d	⊢ ( 𝜑 → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊊ 𝐵 )
87	86	pssned	⊢ ( 𝜑 → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ≠ 𝐵 )
88	87	necomd	⊢ ( 𝜑 → 𝐵 ≠ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
89	84	simp3d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐵 ) = ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
90	4	fveq1i	⊢ ( 𝐻 ‘ 𝐵 ) = ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 )
91	4	fveq1i	⊢ ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
92	89 90 91	3eqtr3g	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 ) = ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
93	9 85	sselpwd	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐴 )
94	72 93	fvco3d	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) )
95	86	pssssd	⊢ ( 𝜑 → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊆ 𝐵 )
96	95 85	sstrd	⊢ ( 𝜑 → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊆ 𝐴 )
97	9 96	sselpwd	⊢ ( 𝜑 → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ 𝒫 𝐴 )
98	72 97	fvco3d	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) )
99	92 94 98	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) )
100	99	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) )
101		eqid	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) )
102		eqeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝐵 = 𝐴 ) )
103		id	⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
104	102 103	ifbieq2d	⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) = if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) )
105		ifcl	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝐵 ∈ 𝒫 𝐴 ) → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) ∈ 𝒫 𝐴 )
106	56 93 105	sylancr	⊢ ( 𝜑 → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) ∈ 𝒫 𝐴 )
107	101 104 93 106	fvmptd3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) = if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) )
108		pssne	⊢ ( 𝐵 ⊊ 𝐴 → 𝐵 ≠ 𝐴 )
109	108	neneqd	⊢ ( 𝐵 ⊊ 𝐴 → ¬ 𝐵 = 𝐴 )
110	109	iffalsed	⊢ ( 𝐵 ⊊ 𝐴 → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) = 𝐵 )
111	107 110	sylan9eq	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) = 𝐵 )
112	111	fveq2d	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ 𝐵 ) )
113		eqeq1	⊢ ( 𝑥 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) → ( 𝑥 = 𝐴 ↔ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 ) )
114		id	⊢ ( 𝑥 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) → 𝑥 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
115	113 114	ifbieq2d	⊢ ( 𝑥 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) = if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
116		ifcl	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ 𝒫 𝐴 ) → if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ∈ 𝒫 𝐴 )
117	56 97 116	sylancr	⊢ ( 𝜑 → if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ∈ 𝒫 𝐴 )
118	101 115 97 117	fvmptd3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
119	118	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
120		sspsstr	⊢ ( ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴 ) → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊊ 𝐴 )
121	95 120	sylan	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ⊊ 𝐴 )
122	121	pssned	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ≠ 𝐴 )
123	122	neneqd	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ¬ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 )
124	123	iffalsed	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → if ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) = 𝐴 , ∅ , ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
125	119 124	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
126	125	fveq2d	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
127	100 112 126	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝐵 ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
128	93 108	anim12i	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
129		eldifsn	⊢ ( 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴 ) )
130	128 129	sylibr	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
131	130	fvresd	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( 𝐺 ∘ 𝐹 ) ‘ 𝐵 ) )
132	97	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ 𝒫 𝐴 )
133		eldifsn	⊢ ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ 𝒫 𝐴 ∧ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ≠ 𝐴 ) )
134	132 122 133	sylanbrc	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
135	134	fvresd	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) = ( ( 𝐺 ∘ 𝐹 ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
136	127 131 135	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
137		f1of1	⊢ ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ 𝐴 → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1→ 𝐴 )
138	53 137	syl	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1→ 𝐴 )
139	138	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1→ 𝐴 )
140		f1fveq	⊢ ( ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1→ 𝐴 ∧ ( 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ∧ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) → ( ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ↔ 𝐵 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
141	139 130 134 140	syl12anc	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → ( ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺 ∘ 𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) ↔ 𝐵 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
142	136 141	mpbid	⊢ ( ( 𝜑 ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) )
143	142	ex	⊢ ( 𝜑 → ( 𝐵 ⊊ 𝐴 → 𝐵 = ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) ) )
144	143	necon3ad	⊢ ( 𝜑 → ( 𝐵 ≠ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { ( 𝐻 ‘ 𝐵 ) } ) → ¬ 𝐵 ⊊ 𝐴 ) )
145	88 144	mpd	⊢ ( 𝜑 → ¬ 𝐵 ⊊ 𝐴 )
146		npss	⊢ ( ¬ 𝐵 ⊊ 𝐴 ↔ ( 𝐵 ⊆ 𝐴 → 𝐵 = 𝐴 ) )
147	145 146	sylib	⊢ ( 𝜑 → ( 𝐵 ⊆ 𝐴 → 𝐵 = 𝐴 ) )
148	85 147	mpd	⊢ ( 𝜑 → 𝐵 = 𝐴 )
149		eqid	⊢ 𝐵 = 𝐵
150		eqid	⊢ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 )
151	149 150	pm3.2i	⊢ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) )
152		elinel1	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) → 𝑥 ∈ 𝒫 𝐴 )
153		ffvelcdm	⊢ ( ( 𝐻 : 𝒫 𝐴 ⟶ 𝐴 ∧ 𝑥 ∈ 𝒫 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
154	79 152 153	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
155	5 9 154 6	fpwwe	⊢ ( 𝜑 → ( ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐻 ‘ 𝐵 ) ∈ 𝐵 ) ↔ ( 𝐵 = 𝐵 ∧ ( 𝑊 ‘ 𝐵 ) = ( 𝑊 ‘ 𝐵 ) ) ) )
156	151 155	mpbiri	⊢ ( 𝜑 → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ∧ ( 𝐻 ‘ 𝐵 ) ∈ 𝐵 ) )
157	156	simpld	⊢ ( 𝜑 → 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) )
158	5 9	fpwwelem	⊢ ( 𝜑 → ( 𝐵 𝑊 ( 𝑊 ‘ 𝐵 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) ) )
159	157 158	mpbid	⊢ ( 𝜑 → ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ‘ 𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐻 ‘ ( ^◡ ( 𝑊 ‘ 𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) )
160	159	simprld	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) We 𝐵 )
161		fvex	⊢ ( 𝑊 ‘ 𝐵 ) ∈ V
162		weeq1	⊢ ( 𝑟 = ( 𝑊 ‘ 𝐵 ) → ( 𝑟 We 𝐵 ↔ ( 𝑊 ‘ 𝐵 ) We 𝐵 ) )
163	161 162	spcev	⊢ ( ( 𝑊 ‘ 𝐵 ) We 𝐵 → ∃ 𝑟 𝑟 We 𝐵 )
164	160 163	syl	⊢ ( 𝜑 → ∃ 𝑟 𝑟 We 𝐵 )
165		ween	⊢ ( 𝐵 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐵 )
166	164 165	sylibr	⊢ ( 𝜑 → 𝐵 ∈ dom card )
167	148 166	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ dom card )
168		domtri2	⊢ ( ( ω ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
169	23 167 168	sylancr	⊢ ( 𝜑 → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
170		infdju1	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1_o ) ≈ 𝐴 )
171	169 170	biimtrrdi	⊢ ( 𝜑 → ( ¬ 𝐴 ≺ ω → ( 𝐴 ⊔ 1_o ) ≈ 𝐴 ) )
172		ensym	⊢ ( ( 𝐴 ⊔ 1_o ) ≈ 𝐴 → 𝐴 ≈ ( 𝐴 ⊔ 1_o ) )
173	171 172	syl6	⊢ ( 𝜑 → ( ¬ 𝐴 ≺ ω → 𝐴 ≈ ( 𝐴 ⊔ 1_o ) ) )
174	20 173	mt3d	⊢ ( 𝜑 → 𝐴 ≺ ω )
175		2onn	⊢ 2_o ∈ ω
176		nnsdom	⊢ ( 2_o ∈ ω → 2_o ≺ ω )
177	175 176	ax-mp	⊢ 2_o ≺ ω
178		djufi	⊢ ( ( 𝐴 ≺ ω ∧ 2_o ≺ ω ) → ( 𝐴 ⊔ 2_o ) ≺ ω )
179	174 177 178	sylancl	⊢ ( 𝜑 → ( 𝐴 ⊔ 2_o ) ≺ ω )
180		isfinite	⊢ ( ( 𝐴 ⊔ 2_o ) ∈ Fin ↔ ( 𝐴 ⊔ 2_o ) ≺ ω )
181	179 180	sylibr	⊢ ( 𝜑 → ( 𝐴 ⊔ 2_o ) ∈ Fin )
182		sssucid	⊢ 1_o ⊆ suc 1_o
183		df-2o	⊢ 2_o = suc 1_o
184	182 183	sseqtrri	⊢ 1_o ⊆ 2_o
185		xpss2	⊢ ( 1_o ⊆ 2_o → ( { 1_o } × 1_o ) ⊆ ( { 1_o } × 2_o ) )
186	184 185	ax-mp	⊢ ( { 1_o } × 1_o ) ⊆ ( { 1_o } × 2_o )
187		unss2	⊢ ( ( { 1_o } × 1_o ) ⊆ ( { 1_o } × 2_o ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) )
188	186 187	mp1i	⊢ ( 𝜑 → ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) )
189		ssun2	⊢ ( { 1_o } × 2_o ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) )
190		1oex	⊢ 1_o ∈ V
191	190	snid	⊢ 1_o ∈ { 1_o }
192	190	sucid	⊢ 1_o ∈ suc 1_o
193	192 183	eleqtrri	⊢ 1_o ∈ 2_o
194		opelxpi	⊢ ( ( 1_o ∈ { 1_o } ∧ 1_o ∈ 2_o ) → ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 2_o ) )
195	191 193 194	mp2an	⊢ ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 2_o )
196	189 195	sselii	⊢ ⟨ 1_o , 1_o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) )
197		1n0	⊢ 1_o ≠ ∅
198	197	neii	⊢ ¬ 1_o = ∅
199		opelxp1	⊢ ( ⟨ 1_o , 1_o ⟩ ∈ ( { ∅ } × 𝐴 ) → 1_o ∈ { ∅ } )
200		elsni	⊢ ( 1_o ∈ { ∅ } → 1_o = ∅ )
201	199 200	syl	⊢ ( ⟨ 1_o , 1_o ⟩ ∈ ( { ∅ } × 𝐴 ) → 1_o = ∅ )
202	198 201	mto	⊢ ¬ ⟨ 1_o , 1_o ⟩ ∈ ( { ∅ } × 𝐴 )
203		1onn	⊢ 1_o ∈ ω
204		nnord	⊢ ( 1_o ∈ ω → Ord 1_o )
205		ordirr	⊢ ( Ord 1_o → ¬ 1_o ∈ 1_o )
206	203 204 205	mp2b	⊢ ¬ 1_o ∈ 1_o
207		opelxp2	⊢ ( ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 1_o ) → 1_o ∈ 1_o )
208	206 207	mto	⊢ ¬ ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 1_o )
209	202 208	pm3.2ni	⊢ ¬ ( ⟨ 1_o , 1_o ⟩ ∈ ( { ∅ } × 𝐴 ) ∨ ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 1_o ) )
210		elun	⊢ ( ⟨ 1_o , 1_o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ↔ ( ⟨ 1_o , 1_o ⟩ ∈ ( { ∅ } × 𝐴 ) ∨ ⟨ 1_o , 1_o ⟩ ∈ ( { 1_o } × 1_o ) ) )
211	209 210	mtbir	⊢ ¬ ⟨ 1_o , 1_o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) )
212		ssnelpss	⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) → ( ( ⟨ 1_o , 1_o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) ∧ ¬ ⟨ 1_o , 1_o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) ) )
213	196 211 212	mp2ani	⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) )
214	188 213	syl	⊢ ( 𝜑 → ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) )
215		df-dju	⊢ ( 𝐴 ⊔ 1_o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) )
216		df-dju	⊢ ( 𝐴 ⊔ 2_o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) )
217	215 216	psseq12i	⊢ ( ( 𝐴 ⊔ 1_o ) ⊊ ( 𝐴 ⊔ 2_o ) ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 1_o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 2_o ) ) )
218	214 217	sylibr	⊢ ( 𝜑 → ( 𝐴 ⊔ 1_o ) ⊊ ( 𝐴 ⊔ 2_o ) )
219		php3	⊢ ( ( ( 𝐴 ⊔ 2_o ) ∈ Fin ∧ ( 𝐴 ⊔ 1_o ) ⊊ ( 𝐴 ⊔ 2_o ) ) → ( 𝐴 ⊔ 1_o ) ≺ ( 𝐴 ⊔ 2_o ) )
220	181 218 219	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊔ 1_o ) ≺ ( 𝐴 ⊔ 2_o ) )
221		canthp1lem1	⊢ ( 1_o ≺ 𝐴 → ( 𝐴 ⊔ 2_o ) ≼ 𝒫 𝐴 )
222	1 221	syl	⊢ ( 𝜑 → ( 𝐴 ⊔ 2_o ) ≼ 𝒫 𝐴 )
223		sdomdomtr	⊢ ( ( ( 𝐴 ⊔ 1_o ) ≺ ( 𝐴 ⊔ 2_o ) ∧ ( 𝐴 ⊔ 2_o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 1_o ) ≺ 𝒫 𝐴 )
224	220 222 223	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊔ 1_o ) ≺ 𝒫 𝐴 )
225		sdomnen	⊢ ( ( 𝐴 ⊔ 1_o ) ≺ 𝒫 𝐴 → ¬ ( 𝐴 ⊔ 1_o ) ≈ 𝒫 𝐴 )
226	224 225	syl	⊢ ( 𝜑 → ¬ ( 𝐴 ⊔ 1_o ) ≈ 𝒫 𝐴 )
227	13 226	pm2.65i	⊢ ¬ 𝜑

Metamath Proof Explorer

Theorem canthp1lem2

Proof