Metamath Proof Explorer

Theorem ordtypelem7

Description: Lemma for ordtype . ran O is an initial segment of A under the well-order R . (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypotheses ordtypelem.1 ⊢ 𝐹 = recs ( 𝐺 )
ordtypelem.2 ⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
ordtypelem.3 ⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
ordtypelem.5 ⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
ordtypelem.6 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
ordtypelem.7 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
ordtypelem.8 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
Assertion ordtypelem7 ( ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) ∧ 𝑀 ∈ dom 𝑂 ) → ( ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ∨ 𝑁 ∈ ran 𝑂 ) )

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢ 𝐹 = recs ( 𝐺 )
2 ordtypelem.2 ⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
3 ordtypelem.3 ⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4 ordtypelem.5 ⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
5 ordtypelem.6 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
6 ordtypelem.7 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
7 ordtypelem.8 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
8 eldif ⊢ ( 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ↔ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂 ) )
9 1 2 3 4 5 6 7 ordtypelem4 ⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
11 10 fdmd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
12 inss1 ⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ 𝑇
13 1 2 3 4 5 6 7 ordtypelem2 ⊢ ( 𝜑 → Ord 𝑇 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → Ord 𝑇 )
15 ordsson ⊢ ( Ord 𝑇 → 𝑇 ⊆ On )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → 𝑇 ⊆ On )
17 12 16 sstrid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑇 ∩ dom 𝐹 ) ⊆ On )
18 11 17 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → dom 𝑂 ⊆ On )
19 18 sseld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → 𝑀 ∈ On ) )
20 eleq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂 ) )
21 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑂 ‘ 𝑎 ) = ( 𝑂 ‘ 𝑏 ) )
22 21 breq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ↔ ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) )
23 20 22 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ↔ ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) )
24 23 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) ) )
25 eleq1 ⊢ ( 𝑎 = 𝑀 → ( 𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂 ) )
26 fveq2 ⊢ ( 𝑎 = 𝑀 → ( 𝑂 ‘ 𝑎 ) = ( 𝑂 ‘ 𝑀 ) )
27 26 breq1d ⊢ ( 𝑎 = 𝑀 → ( ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ↔ ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
28 25 27 imbi12d ⊢ ( 𝑎 = 𝑀 → ( ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ↔ ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) ) )
29 28 imbi2d ⊢ ( 𝑎 = 𝑀 → ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) ) ) )
30 r19.21v ⊢ ( ∀ 𝑏 ∈ 𝑎 ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) )
31 1 tfr1a ⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 )
32 31 simpri ⊢ Lim dom 𝐹
33 limord ⊢ ( Lim dom 𝐹 → Ord dom 𝐹 )
34 32 33 ax-mp ⊢ Ord dom 𝐹
35 ordin ⊢ ( ( Ord 𝑇 ∧ Ord dom 𝐹 ) → Ord ( 𝑇 ∩ dom 𝐹 ) )
36 14 34 35 sylancl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → Ord ( 𝑇 ∩ dom 𝐹 ) )
37 ordeq ⊢ ( dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) )
38 11 37 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) )
39 36 38 mpbird ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → Ord dom 𝑂 )
40 ordelss ⊢ ( ( Ord dom 𝑂 ∧ 𝑎 ∈ dom 𝑂 ) → 𝑎 ⊆ dom 𝑂 )
41 39 40 sylan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) → 𝑎 ⊆ dom 𝑂 )
42 41 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ dom 𝑂 )
43 pm5.5 ⊢ ( 𝑏 ∈ dom 𝑂 → ( ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ↔ ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) )
44 42 43 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) ∧ 𝑏 ∈ 𝑎 ) → ( ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ↔ ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) )
45 44 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ↔ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) )
46 eldifn ⊢ ( 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) → ¬ 𝑁 ∈ ran 𝑂 )
47 46 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ¬ 𝑁 ∈ ran 𝑂 )
48 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
49 48 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑂 Fn ( 𝑇 ∩ dom 𝐹 ) )
50 simprl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ∈ dom 𝑂 )
51 48 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
52 50 51 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) )
53 fnfvelrn ⊢ ( ( 𝑂 Fn ( 𝑇 ∩ dom 𝐹 ) ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝑂 ‘ 𝑎 ) ∈ ran 𝑂 )
54 49 52 53 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) ∈ ran 𝑂 )
55 eleq1 ⊢ ( ( 𝑂 ‘ 𝑎 ) = 𝑁 → ( ( 𝑂 ‘ 𝑎 ) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂 ) )
56 54 55 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝑂 ‘ 𝑎 ) = 𝑁 → 𝑁 ∈ ran 𝑂 ) )
57 47 56 mtod ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ¬ ( 𝑂 ‘ 𝑎 ) = 𝑁 )
58 breq1 ⊢ ( 𝑢 = 𝑁 → ( 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ↔ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
59 58 notbid ⊢ ( 𝑢 = 𝑁 → ( ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ↔ ¬ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
60 1 2 3 4 5 6 7 ordtypelem1 ⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
62 61 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) )
63 52 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ∈ 𝑇 )
64 63 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
65 62 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
66 simpll ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝜑 )
67 1 2 3 4 5 6 7 ordtypelem3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
68 66 52 67 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
69 65 68 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
70 breq2 ⊢ ( 𝑣 = ( 𝑂 ‘ 𝑎 ) → ( 𝑢 𝑅 𝑣 ↔ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
71 70 notbid ⊢ ( 𝑣 = ( 𝑂 ‘ 𝑎 ) → ( ¬ 𝑢 𝑅 𝑣 ↔ ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
72 71 ralbidv ⊢ ( 𝑣 = ( 𝑂 ‘ 𝑎 ) → ( ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ↔ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
73 72 elrab ⊢ ( ( 𝑂 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ↔ ( ( 𝑂 ‘ 𝑎 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∧ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
74 73 simprbi ⊢ ( ( 𝑂 ‘ 𝑎 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } → ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) )
75 69 74 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 ( 𝑂 ‘ 𝑎 ) )
76 breq2 ⊢ ( 𝑤 = 𝑁 → ( 𝑗 𝑅 𝑤 ↔ 𝑗 𝑅 𝑁 ) )
77 76 ralbidv ⊢ ( 𝑤 = 𝑁 → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 ↔ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑁 ) )
78 eldifi ⊢ ( 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) → 𝑁 ∈ 𝐴 )
79 78 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑁 ∈ 𝐴 )
80 simprr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 )
81 41 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ⊆ dom 𝑂 )
82 48 81 fssdmd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ⊆ ( 𝑇 ∩ dom 𝐹 ) )
83 82 12 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ⊆ 𝑇 )
84 fveq1 ⊢ ( 𝑂 = ( 𝐹 ↾ 𝑇 ) → ( 𝑂 ‘ 𝑏 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑏 ) )
85 ssel2 ⊢ ( ( 𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝑇 )
86 85 fvresd ⊢ ( ( 𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎 ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
87 84 86 sylan9eq ⊢ ( ( 𝑂 = ( 𝐹 ↾ 𝑇 ) ∧ ( 𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎 ) ) → ( 𝑂 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
88 87 anassrs ⊢ ( ( ( 𝑂 = ( 𝐹 ↾ 𝑇 ) ∧ 𝑎 ⊆ 𝑇 ) ∧ 𝑏 ∈ 𝑎 ) → ( 𝑂 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
89 88 breq1d ⊢ ( ( ( 𝑂 = ( 𝐹 ↾ 𝑇 ) ∧ 𝑎 ⊆ 𝑇 ) ∧ 𝑏 ∈ 𝑎 ) → ( ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ↔ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
90 89 ralbidva ⊢ ( ( 𝑂 = ( 𝐹 ↾ 𝑇 ) ∧ 𝑎 ⊆ 𝑇 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ↔ ∀ 𝑏 ∈ 𝑎 ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
91 61 83 90 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ↔ ∀ 𝑏 ∈ 𝑎 ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
92 80 91 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ∀ 𝑏 ∈ 𝑎 ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 )
93 31 simpli ⊢ Fun 𝐹
94 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
95 93 94 mpbi ⊢ 𝐹 Fn dom 𝐹
96 inss2 ⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ dom 𝐹
97 82 96 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑎 ⊆ dom 𝐹 )
98 breq1 ⊢ ( 𝑗 = ( 𝐹 ‘ 𝑏 ) → ( 𝑗 𝑅 𝑁 ↔ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
99 98 ralima ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑁 ↔ ∀ 𝑏 ∈ 𝑎 ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
100 95 97 99 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑁 ↔ ∀ 𝑏 ∈ 𝑎 ( 𝐹 ‘ 𝑏 ) 𝑅 𝑁 ) )
101 92 100 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑁 )
102 77 79 101 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑁 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑎 ) 𝑗 𝑅 𝑤 } )
103 59 75 102 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ¬ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) )
104 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
105 6 104 syl ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
106 105 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → 𝑅 Or 𝐴 )
107 48 52 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) ∈ 𝐴 )
108 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝑂 ‘ 𝑎 ) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴 ) ) → ( ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ↔ ¬ ( ( 𝑂 ‘ 𝑎 ) = 𝑁 ∨ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) ) )
109 106 107 79 108 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ↔ ¬ ( ( 𝑂 ‘ 𝑎 ) = 𝑁 ∨ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) ) )
110 ioran ⊢ ( ¬ ( ( 𝑂 ‘ 𝑎 ) = 𝑁 ∨ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) ↔ ( ¬ ( 𝑂 ‘ 𝑎 ) = 𝑁 ∧ ¬ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) )
111 109 110 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ↔ ( ¬ ( 𝑂 ‘ 𝑎 ) = 𝑁 ∧ ¬ 𝑁 𝑅 ( 𝑂 ‘ 𝑎 ) ) ) )
112 57 103 111 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ ( 𝑎 ∈ dom 𝑂 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 )
113 112 expr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) )
114 45 113 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) ∧ 𝑎 ∈ dom 𝑂 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) )
115 114 ex ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) )
116 115 com23 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) )
117 116 a2i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) )
118 117 a1i ⊢ ( 𝑎 ∈ On → ( ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ∀ 𝑏 ∈ 𝑎 ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) ) )
119 30 118 syl5bi ⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑏 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑏 ) 𝑅 𝑁 ) ) → ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑎 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑎 ) 𝑅 𝑁 ) ) ) )
120 24 29 119 tfis3 ⊢ ( 𝑀 ∈ On → ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) ) )
121 120 com3l ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑀 ∈ On → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) ) )
122 19 121 mpdd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝐴 ∖ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
123 8 122 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂 ) ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
124 123 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) ∧ ¬ 𝑁 ∈ ran 𝑂 ) → ( 𝑀 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
125 124 impancom ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) ∧ 𝑀 ∈ dom 𝑂 ) → ( ¬ 𝑁 ∈ ran 𝑂 → ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
126 125 orrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝑁 ∈ ran 𝑂 ∨ ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ) )
127 126 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) ∧ 𝑀 ∈ dom 𝑂 ) → ( ( 𝑂 ‘ 𝑀 ) 𝑅 𝑁 ∨ 𝑁 ∈ ran 𝑂 ) )