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

Metamath Proof Explorer

Theorem canthp1lem2

Proof