This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem harwdom

Description: The value of the Hartogs function at a set X is weakly dominated by ~P ( X X. X ) . This follows from a more precise analysis of the bound used in hartogs to prove that ( harX ) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harwdom ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) ≼* 𝒫 ( 𝑋 × 𝑋 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
2 eqid ⊢ { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑓 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑓 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑓 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑓 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
3 1 2 hartogslem1 ⊢ ( dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ Fun { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∧ ( 𝑋 ∈ 𝑉 → ran { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝑋 } ) )
4 3 simp2i ⊢ Fun { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
5 3 simp1i ⊢ dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ⊆ 𝒫 ( 𝑋 × 𝑋 )
6 sqxpexg ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 × 𝑋 ) ∈ V )
7 6 pwexd ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ( 𝑋 × 𝑋 ) ∈ V )
8 ssexg ⊢ ( ( dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ 𝒫 ( 𝑋 × 𝑋 ) ∈ V ) → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V )
9 5 7 8 sylancr ⊢ ( 𝑋 ∈ 𝑉 → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V )
10 funex ⊢ ( ( Fun { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∧ dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V ) → { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V )
11 4 9 10 sylancr ⊢ ( 𝑋 ∈ 𝑉 → { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V )
12 funfn ⊢ ( Fun { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ↔ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } Fn dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } )
13 4 12 mpbi ⊢ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } Fn dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
14 13 a1i ⊢ ( 𝑋 ∈ 𝑉 → { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } Fn dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } )
15 3 simp3i ⊢ ( 𝑋 ∈ 𝑉 → ran { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝑋 } )
16 harval ⊢ ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝑋 } )
17 15 16 eqtr4d ⊢ ( 𝑋 ∈ 𝑉 → ran { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = ( har ‘ 𝑋 ) )
18 df-fo ⊢ ( { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } : dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } –onto→ ( har ‘ 𝑋 ) ↔ ( { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } Fn dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∧ ran { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } = ( har ‘ 𝑋 ) ) )
19 14 17 18 sylanbrc ⊢ ( 𝑋 ∈ 𝑉 → { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } : dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } –onto→ ( har ‘ 𝑋 ) )
20 fowdom ⊢ ( ( { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∈ V ∧ { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } : dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } –onto→ ( har ‘ 𝑋 ) ) → ( har ‘ 𝑋 ) ≼* dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } )
21 11 19 20 syl2anc ⊢ ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) ≼* dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } )
22 ssdomg ⊢ ( 𝒫 ( 𝑋 × 𝑋 ) ∈ V → ( dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ⊆ 𝒫 ( 𝑋 × 𝑋 ) → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼ 𝒫 ( 𝑋 × 𝑋 ) ) )
23 7 5 22 mpisyl ⊢ ( 𝑋 ∈ 𝑉 → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼ 𝒫 ( 𝑋 × 𝑋 ) )
24 domwdom ⊢ ( dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼ 𝒫 ( 𝑋 × 𝑋 ) → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼* 𝒫 ( 𝑋 × 𝑋 ) )
25 23 24 syl ⊢ ( 𝑋 ∈ 𝑉 → dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼* 𝒫 ( 𝑋 × 𝑋 ) )
26 wdomtr ⊢ ( ( ( har ‘ 𝑋 ) ≼* dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ∧ dom { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } ≼* 𝒫 ( 𝑋 × 𝑋 ) ) → ( har ‘ 𝑋 ) ≼* 𝒫 ( 𝑋 × 𝑋 ) )
27 21 25 26 syl2anc ⊢ ( 𝑋 ∈ 𝑉 → ( har ‘ 𝑋 ) ≼* 𝒫 ( 𝑋 × 𝑋 ) )