Metamath Proof Explorer

Theorem noinffv

Description: The value of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinffv.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion noinffv ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑇 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 noinffv.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 iffalse ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
3 1 2 syl5eq ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
4 3 fveq1d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ( 𝑇 ‘ 𝐺 ) = ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) )
5 4 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑇 ‘ 𝐺 ) = ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) )
6 dmeq ⊢ ( 𝑢 = 𝑈 → dom 𝑢 = dom 𝑈 )
7 6 eleq2d ⊢ ( 𝑢 = 𝑈 → ( 𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑈 ) )
8 breq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 <s 𝑣 ↔ 𝑈 <s 𝑣 ) )
9 8 notbid ⊢ ( 𝑢 = 𝑈 → ( ¬ 𝑢 <s 𝑣 ↔ ¬ 𝑈 <s 𝑣 ) )
10 reseq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )
11 10 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
12 9 11 imbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
13 12 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
14 7 13 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ↔ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
15 14 rspcev ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
16 15 3impb ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
17 16 3ad2ant3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
18 simp32 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ dom 𝑈 )
19 eleq1 ⊢ ( 𝑦 = 𝐺 → ( 𝑦 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢 ) )
20 suceq ⊢ ( 𝑦 = 𝐺 → suc 𝑦 = suc 𝐺 )
21 20 reseq2d ⊢ ( 𝑦 = 𝐺 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝐺 ) )
22 20 reseq2d ⊢ ( 𝑦 = 𝐺 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝐺 ) )
23 21 22 eqeq12d ⊢ ( 𝑦 = 𝐺 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
24 23 imbi2d ⊢ ( 𝑦 = 𝐺 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
25 24 ralbidv ⊢ ( 𝑦 = 𝐺 → ( ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
26 19 25 anbi12d ⊢ ( 𝑦 = 𝐺 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
27 26 rexbidv ⊢ ( 𝑦 = 𝐺 → ( ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
28 27 elabg ⊢ ( 𝐺 ∈ dom 𝑈 → ( 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
29 18 28 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
30 17 29 mpbird ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
31 eleq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢 ) )
32 suceq ⊢ ( 𝑔 = 𝐺 → suc 𝑔 = suc 𝐺 )
33 32 reseq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑢 ↾ suc 𝐺 ) )
34 32 reseq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑣 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝐺 ) )
35 33 34 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
36 35 imbi2d ⊢ ( 𝑔 = 𝐺 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
37 36 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
38 fveqeq2 ⊢ ( 𝑔 = 𝐺 → ( ( 𝑢 ‘ 𝑔 ) = 𝑥 ↔ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
39 31 37 38 3anbi123d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
40 39 rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
41 40 iotabidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) = ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
42 eqid ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
43 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) ∈ V
44 41 42 43 fvmpt ⊢ ( 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } → ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) = ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
45 30 44 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) = ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
46 simp1 ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → 𝑈 ∈ 𝐵 )
47 simp2 ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → 𝐺 ∈ dom 𝑈 )
48 simp3 ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
49 eqidd ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ( 𝑈 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) )
50 fveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) )
51 50 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ↔ ( 𝑈 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) )
52 7 13 51 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑈 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ) )
53 52 rspcev ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑈 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) )
54 46 47 48 49 53 syl13anc ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) )
55 54 3ad2ant3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) )
56 fvex ⊢ ( 𝑈 ‘ 𝐺 ) ∈ V
57 eqid ⊢ ( 𝑢 ‘ 𝐺 ) = ( 𝑢 ‘ 𝐺 )
58 fvex ⊢ ( 𝑢 ‘ 𝐺 ) ∈ V
59 eqeq2 ⊢ ( 𝑥 = ( 𝑢 ‘ 𝐺 ) → ( ( 𝑢 ‘ 𝐺 ) = 𝑥 ↔ ( 𝑢 ‘ 𝐺 ) = ( 𝑢 ‘ 𝐺 ) ) )
60 59 3anbi3d ⊢ ( 𝑥 = ( 𝑢 ‘ 𝐺 ) → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑢 ‘ 𝐺 ) ) ) )
61 58 60 spcev ⊢ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑢 ‘ 𝐺 ) ) → ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
62 57 61 mp3an3 ⊢ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
63 62 reximi ⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑢 ∈ 𝐵 ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
64 rexcom4 ⊢ ( ∃ 𝑢 ∈ 𝐵 ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
65 63 64 sylib ⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
66 16 65 syl ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
67 66 3ad2ant3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
68 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐵 ⊆ No )
69 noinfprefixmo ⊢ ( 𝐵 ⊆ No → ∃* 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
70 68 69 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃* 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
71 df-eu ⊢ ( ∃! 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ( ∃ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ∃* 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) )
72 67 70 71 sylanbrc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃! 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )
73 eqeq2 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝐺 ) → ( ( 𝑢 ‘ 𝐺 ) = 𝑥 ↔ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) )
74 73 3anbi3d ⊢ ( 𝑥 = ( 𝑈 ‘ 𝐺 ) → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ) )
75 74 rexbidv ⊢ ( 𝑥 = ( 𝑈 ‘ 𝐺 ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ) )
76 75 iota2 ⊢ ( ( ( 𝑈 ‘ 𝐺 ) ∈ V ∧ ∃! 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ↔ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) = ( 𝑈 ‘ 𝐺 ) ) )
77 56 72 76 sylancr ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) ) ↔ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) = ( 𝑈 ‘ 𝐺 ) ) )
78 55 77 mpbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) = ( 𝑈 ‘ 𝐺 ) )
79 5 45 78 3eqtrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑇 ‘ 𝐺 ) = ( 𝑈 ‘ 𝐺 ) )