Metamath Proof Explorer

Theorem satfv1lem

Description: Lemma for satfv1 . (Contributed by AV, 9-Nov-2023)

Ref Expression
Assertion satfv1lem ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑏 = ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) → ( 𝑏 ‘ 𝐼 ) = ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) )
2 fveq1 ⊢ ( 𝑏 = ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) → ( 𝑏 ‘ 𝐽 ) = ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) )
3 1 2 breq12d ⊢ ( 𝑏 = ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) → ( ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) )
4 3 elrab ⊢ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) )
5 4 a1i ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ) )
6 elex ⊢ ( 𝑁 ∈ ω → 𝑁 ∈ V )
7 6 3ad2ant1 ⊢ ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → 𝑁 ∈ V )
8 7 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → 𝑁 ∈ V )
9 simpr ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → 𝑧 ∈ 𝑀 )
10 8 9 fsnd ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → { ⟨ 𝑁 , 𝑧 ⟩ } : { 𝑁 } ⟶ 𝑀 )
11 elmapex ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝑀 ∈ V ∧ ω ∈ V ) )
12 11 simpld ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → 𝑀 ∈ V )
13 12 adantr ⊢ ( ( 𝑎 ∈ ( 𝑀 ↑m ω ) ∧ 𝑧 ∈ 𝑀 ) → 𝑀 ∈ V )
14 snex ⊢ { 𝑁 } ∈ V
15 14 a1i ⊢ ( ( 𝑎 ∈ ( 𝑀 ↑m ω ) ∧ 𝑧 ∈ 𝑀 ) → { 𝑁 } ∈ V )
16 13 15 elmapd ⊢ ( ( 𝑎 ∈ ( 𝑀 ↑m ω ) ∧ 𝑧 ∈ 𝑀 ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ∈ ( 𝑀 ↑m { 𝑁 } ) ↔ { ⟨ 𝑁 , 𝑧 ⟩ } : { 𝑁 } ⟶ 𝑀 ) )
17 16 adantll ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ∈ ( 𝑀 ↑m { 𝑁 } ) ↔ { ⟨ 𝑁 , 𝑧 ⟩ } : { 𝑁 } ⟶ 𝑀 ) )
18 10 17 mpbird ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → { ⟨ 𝑁 , 𝑧 ⟩ } ∈ ( 𝑀 ↑m { 𝑁 } ) )
19 elmapi ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → 𝑎 : ω ⟶ 𝑀 )
20 difssd ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ω ∖ { 𝑁 } ) ⊆ ω )
21 19 20 fssresd ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) : ( ω ∖ { 𝑁 } ) ⟶ 𝑀 )
22 omex ⊢ ω ∈ V
23 22 difexi ⊢ ( ω ∖ { 𝑁 } ) ∈ V
24 23 a1i ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ω ∖ { 𝑁 } ) ∈ V )
25 12 24 elmapd ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ∈ ( 𝑀 ↑m ( ω ∖ { 𝑁 } ) ) ↔ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) : ( ω ∖ { 𝑁 } ) ⟶ 𝑀 ) )
26 21 25 mpbird ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ∈ ( 𝑀 ↑m ( ω ∖ { 𝑁 } ) ) )
27 26 adantl ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ∈ ( 𝑀 ↑m ( ω ∖ { 𝑁 } ) ) )
28 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ∈ ( 𝑀 ↑m ( ω ∖ { 𝑁 } ) ) )
29 res0 ⊢ ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ∅ ) = ∅
30 res0 ⊢ ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ∅ ) = ∅
31 29 30 eqtr4i ⊢ ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ∅ ) = ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ∅ )
32 disjdif ⊢ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) = ∅
33 32 reseq2i ⊢ ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) = ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ∅ )
34 32 reseq2i ⊢ ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) = ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ∅ )
35 31 33 34 3eqtr4i ⊢ ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) = ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) )
36 35 a1i ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) = ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) )
37 elmapresaun ⊢ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∈ ( 𝑀 ↑m { 𝑁 } ) ∧ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ∈ ( 𝑀 ↑m ( ω ∖ { 𝑁 } ) ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) = ( ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ↾ ( { 𝑁 } ∩ ( ω ∖ { 𝑁 } ) ) ) ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) ) )
38 18 28 36 37 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) ) )
39 uncom ⊢ ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) = ( ( ω ∖ { 𝑁 } ) ∪ { 𝑁 } )
40 difsnid ⊢ ( 𝑁 ∈ ω → ( ( ω ∖ { 𝑁 } ) ∪ { 𝑁 } ) = ω )
41 39 40 syl5req ⊢ ( 𝑁 ∈ ω → ω = ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ω = ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) )
43 42 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ω = ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) )
44 43 oveq2d ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( 𝑀 ↑m ω ) = ( 𝑀 ↑m ( { 𝑁 } ∪ ( ω ∖ { 𝑁 } ) ) ) )
45 38 44 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) )
46 ibar ⊢ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ) )
47 46 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ) )
48 47 bicomd ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) )
49 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → 𝑁 ∈ ω )
50 eqid ⊢ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) = ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) )
51 49 9 50 fvsnun1 ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) = 𝑧 )
52 51 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) = 𝑧 )
53 52 52 breq12d ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ 𝑧 𝐸 𝑧 ) )
54 53 adantl ⊢ ( ( 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ 𝑧 𝐸 𝑧 ) )
55 fveq2 ⊢ ( 𝐽 = 𝑁 → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) = ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) )
56 55 breq2d ⊢ ( 𝐽 = 𝑁 → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ) )
57 ifptru ⊢ ( 𝐽 = 𝑁 → ( if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ 𝑧 𝐸 𝑧 ) )
58 56 57 bibi12d ⊢ ( 𝐽 = 𝑁 → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ 𝑧 𝐸 𝑧 ) ) )
59 58 adantr ⊢ ( ( 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ 𝑧 𝐸 𝑧 ) ) )
60 54 59 mpbird ⊢ ( ( 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
61 52 adantl ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) = 𝑧 )
62 49 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → 𝑁 ∈ ω )
63 62 adantl ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝑁 ∈ ω )
64 9 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → 𝑧 ∈ 𝑀 )
65 64 adantl ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝑧 ∈ 𝑀 )
66 neqne ⊢ ( ¬ 𝐽 = 𝑁 → 𝐽 ≠ 𝑁 )
67 simpll3 ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → 𝐽 ∈ ω )
68 67 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → 𝐽 ∈ ω )
69 66 68 anim12ci ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( 𝐽 ∈ ω ∧ 𝐽 ≠ 𝑁 ) )
70 eldifsn ⊢ ( 𝐽 ∈ ( ω ∖ { 𝑁 } ) ↔ ( 𝐽 ∈ ω ∧ 𝐽 ≠ 𝑁 ) )
71 69 70 sylibr ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝐽 ∈ ( ω ∖ { 𝑁 } ) )
72 63 65 50 71 fvsnun2 ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) = ( 𝑎 ‘ 𝐽 ) )
73 61 72 breq12d ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
74 ifpfal ⊢ ( ¬ 𝐽 = 𝑁 → ( if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
75 74 bicomd ⊢ ( ¬ 𝐽 = 𝑁 → ( 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
76 75 adantr ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
77 73 76 bitrd ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
78 60 77 pm2.61ian ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
79 78 adantl ⊢ ( ( 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
80 fveq2 ⊢ ( 𝐼 = 𝑁 → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) = ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) )
81 80 breq1d ⊢ ( 𝐼 = 𝑁 → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) )
82 ifptru ⊢ ( 𝐼 = 𝑁 → ( if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
83 81 82 bibi12d ⊢ ( 𝐼 = 𝑁 → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
84 83 adantr ⊢ ( ( 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
85 79 84 mpbird ⊢ ( ( 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
86 62 adantl ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝑁 ∈ ω )
87 64 adantl ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝑧 ∈ 𝑀 )
88 neqne ⊢ ( ¬ 𝐼 = 𝑁 → 𝐼 ≠ 𝑁 )
89 simpll2 ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → 𝐼 ∈ ω )
90 89 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → 𝐼 ∈ ω )
91 88 90 anim12ci ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( 𝐼 ∈ ω ∧ 𝐼 ≠ 𝑁 ) )
92 eldifsn ⊢ ( 𝐼 ∈ ( ω ∖ { 𝑁 } ) ↔ ( 𝐼 ∈ ω ∧ 𝐼 ≠ 𝑁 ) )
93 91 92 sylibr ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → 𝐼 ∈ ( ω ∖ { 𝑁 } ) )
94 86 87 50 93 fvsnun2 ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) = ( 𝑎 ‘ 𝐼 ) )
95 52 adantl ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) = 𝑧 )
96 94 95 breq12d ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) )
97 96 adantl ⊢ ( ( 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) )
98 55 breq2d ⊢ ( 𝐽 = 𝑁 → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ) )
99 ifptru ⊢ ( 𝐽 = 𝑁 → ( if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) )
100 98 99 bibi12d ⊢ ( 𝐽 = 𝑁 → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) ) )
101 100 adantr ⊢ ( ( 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝑁 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) ) )
102 97 101 mpbird ⊢ ( ( 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
103 94 adantl ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) = ( 𝑎 ‘ 𝐼 ) )
104 72 adantrl ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) = ( 𝑎 ‘ 𝐽 ) )
105 103 104 breq12d ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
106 ifpfal ⊢ ( ¬ 𝐽 = 𝑁 → ( if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
107 106 bicomd ⊢ ( ¬ 𝐽 = 𝑁 → ( ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
108 107 adantr ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
109 105 108 bitrd ⊢ ( ( ¬ 𝐽 = 𝑁 ∧ ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
110 102 109 pm2.61ian ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
111 ifpfal ⊢ ( ¬ 𝐼 = 𝑁 → ( if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ↔ if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
112 111 bicomd ⊢ ( ¬ 𝐼 = 𝑁 → ( if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
113 112 adantr ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
114 110 113 bitrd ⊢ ( ( ¬ 𝐼 = 𝑁 ∧ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
115 85 114 pm2.61ian ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
116 48 115 bitrd ⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) ∧ ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
117 45 116 mpdan ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ ( 𝑀 ↑m ω ) ∧ ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐼 ) 𝐸 ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ‘ 𝐽 ) ) ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
118 5 117 bitrd ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) ∧ 𝑧 ∈ 𝑀 ) → ( ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } ↔ if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
119 118 ralbidva ⊢ ( ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } ↔ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
120 119 rabbidva ⊢ ( ( 𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑁 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑁 } ) ) ) ∈ { 𝑏 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑏 ‘ 𝐼 ) 𝐸 ( 𝑏 ‘ 𝐽 ) } } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑁 , if- ( 𝐽 = 𝑁 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑁 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } )