Metamath Proof Explorer

Theorem satfdm

Description: The domain of the satisfaction predicate as function over wff codes does not depend on the model M and the binary relation E on M . (Contributed by AV, 13-Oct-2023)

Ref Expression
Assertion satfdm ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
2 1 dmeqd ⊢ ( 𝑥 = ∅ → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
3 fveq2 ⊢ ( 𝑥 = ∅ → ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) )
4 3 dmeqd ⊢ ( 𝑥 = ∅ → dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) )
5 2 4 eqeq12d ⊢ ( 𝑥 = ∅ → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) ) )
6 5 imbi2d ⊢ ( 𝑥 = ∅ → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
8 7 dmeqd ⊢ ( 𝑥 = 𝑦 → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
9 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) )
10 9 dmeqd ⊢ ( 𝑥 = 𝑦 → dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) )
11 8 10 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) ) )
13 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) )
14 13 dmeqd ⊢ ( 𝑥 = suc 𝑦 → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) )
15 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) )
16 15 dmeqd ⊢ ( 𝑥 = suc 𝑦 → dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) )
18 17 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) ) )
19 fveq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )
20 19 dmeqd ⊢ ( 𝑥 = 𝑛 → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) )
22 21 dmeqd ⊢ ( 𝑥 = 𝑛 → dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) )
23 20 22 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑥 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) ) ) )
25 rexcom4 ⊢ ( ∃ 𝑣 ∈ ω ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑦 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) )
26 25 rexbii ⊢ ( ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑢 ∈ ω ∃ 𝑦 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) )
27 ovex ⊢ ( 𝑀 ↑m ω ) ∈ V
28 27 rabex ⊢ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ∈ V
29 28 isseti ⊢ ∃ 𝑦 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) }
30 ovex ⊢ ( 𝑁 ↑m ω ) ∈ V
31 30 rabex ⊢ { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ∈ V
32 31 isseti ⊢ ∃ 𝑧 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) }
33 29 32 2th ⊢ ( ∃ 𝑦 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ↔ ∃ 𝑧 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } )
34 33 anbi2i ⊢ ( ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ ∃ 𝑦 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ ∃ 𝑧 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
35 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ ∃ 𝑦 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) )
36 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) ↔ ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ ∃ 𝑧 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
37 34 35 36 3bitr4i ⊢ ( ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
38 37 rexbii ⊢ ( ∃ 𝑣 ∈ ω ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑣 ∈ ω ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
39 38 rexbii ⊢ ( ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ∃ 𝑦 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
40 rexcom4 ⊢ ( ∃ 𝑢 ∈ ω ∃ 𝑦 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) )
41 26 39 40 3bitr3ri ⊢ ( ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
42 rexcom4 ⊢ ( ∃ 𝑣 ∈ ω ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑧 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
43 42 rexbii ⊢ ( ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ∃ 𝑧 ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑢 ∈ ω ∃ 𝑧 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
44 41 43 bitri ⊢ ( ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑢 ∈ ω ∃ 𝑧 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
45 rexcom4 ⊢ ( ∃ 𝑢 ∈ ω ∃ 𝑧 ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
46 44 45 bitri ⊢ ( ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) ↔ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) )
47 46 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) }
48 eqid ⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
49 48 satfv0 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } )
50 49 dmeqd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } )
51 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) }
52 50 51 eqtrdi ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } )
53 52 adantr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐸 ( 𝑎 ‘ 𝑣 ) } ) } )
54 eqid ⊢ ( 𝑁 Sat 𝐹 ) = ( 𝑁 Sat 𝐹 )
55 54 satfv0 ⊢ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) → ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) } )
56 55 dmeqd ⊢ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) → dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) = dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) } )
57 dmopab ⊢ dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) }
58 56 57 eqtrdi ⊢ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) → dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) } )
59 58 adantl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑢 ∈ ω ∃ 𝑣 ∈ ω ( 𝑥 = ( 𝑢 ∈𝑔 𝑣 ) ∧ 𝑧 = { 𝑎 ∈ ( 𝑁 ↑m ω ) ∣ ( 𝑎 ‘ 𝑢 ) 𝐹 ( 𝑎 ‘ 𝑣 ) } ) } )
60 47 53 59 3eqtr4a ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ ∅ ) )
61 pm2.27 ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) )
62 61 adantl ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) )
63 simpr ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) )
64 simprl ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) )
65 simpl ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → 𝑦 ∈ ω )
66 df-3an ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑦 ∈ ω ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑦 ∈ ω ) )
67 64 65 66 sylanbrc ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑦 ∈ ω ) )
68 satfdmlem ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑦 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) ) )
69 67 68 sylan ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) ) )
70 simprr ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) )
71 df-3an ⊢ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ∧ 𝑦 ∈ ω ) ↔ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ∧ 𝑦 ∈ ω ) )
72 70 65 71 sylanbrc ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ∧ 𝑦 ∈ ω ) )
73 id ⊢ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) )
74 73 eqcomd ⊢ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) → dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) )
75 satfdmlem ⊢ ( ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ∧ 𝑦 ∈ ω ) ∧ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ) → ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
76 72 74 75 syl2an ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) )
77 69 76 impbid ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) ) )
78 27 difexi ⊢ ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ∈ V
79 78 isseti ⊢ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) )
80 79 biantru ⊢ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ↔ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
81 80 bicomi ⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
82 81 rexbii ⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) )
83 27 rabex ⊢ { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ∈ V
84 83 isseti ⊢ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) }
85 84 biantru ⊢ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ↔ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
86 85 bicomi ⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) )
87 86 rexbii ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) )
88 82 87 orbi12i ⊢ ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
89 88 rexbii ⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) )
90 30 difexi ⊢ ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ∈ V
91 90 isseti ⊢ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) )
92 91 biantru ⊢ ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ↔ ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
93 92 bicomi ⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) )
94 93 rexbii ⊢ ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) )
95 30 rabex ⊢ { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ∈ V
96 95 isseti ⊢ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) }
97 96 biantru ⊢ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ↔ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
98 97 bicomi ⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) )
99 98 rexbii ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) )
100 94 99 orbi12i ⊢ ( ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) )
101 100 rexbii ⊢ ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ) )
102 77 89 101 3bitr4g ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ) )
103 19.42v ⊢ ( ∃ 𝑤 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
104 103 bicomi ⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑤 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
105 104 rexbii ⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∃ 𝑤 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
106 rexcom4 ⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∃ 𝑤 ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑤 ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
107 105 106 bitri ⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑤 ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) )
108 19.42v ⊢ ( ∃ 𝑤 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
109 108 bicomi ⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑤 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
110 109 rexbii ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑤 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
111 rexcom4 ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑤 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑤 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
112 110 111 bitri ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ↔ ∃ 𝑤 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) )
113 107 112 orbi12i ⊢ ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑤 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
114 19.43 ⊢ ( ∃ 𝑤 ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑤 ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑤 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
115 114 bicomi ⊢ ( ( ∃ 𝑤 ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑤 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑤 ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
116 113 115 bitri ⊢ ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑤 ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
117 116 rexbii ⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∃ 𝑤 ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
118 rexcom4 ⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∃ 𝑤 ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑤 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
119 117 118 bitri ⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ ∃ 𝑤 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ ∃ 𝑤 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑤 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) )
120 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
121 120 bicomi ⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ∃ 𝑧 ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
122 121 rexbii ⊢ ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∃ 𝑧 ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
123 rexcom4 ⊢ ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∃ 𝑧 ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ∃ 𝑧 ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
124 122 123 bitri ⊢ ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ↔ ∃ 𝑧 ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) )
125 19.42v ⊢ ( ∃ 𝑧 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
126 125 bicomi ⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ∃ 𝑧 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
127 126 rexbii ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑧 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
128 rexcom4 ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑧 ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ∃ 𝑧 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
129 127 128 bitri ⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ↔ ∃ 𝑧 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) )
130 124 129 orbi12i ⊢ ( ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ( ∃ 𝑧 ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑧 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
131 19.43 ⊢ ( ∃ 𝑧 ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ( ∃ 𝑧 ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑧 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
132 131 bicomi ⊢ ( ( ∃ 𝑧 ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑧 ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑧 ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
133 130 132 bitri ⊢ ( ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑧 ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
134 133 rexbii ⊢ ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∃ 𝑧 ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
135 rexcom4 ⊢ ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∃ 𝑧 ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑧 ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
136 134 135 bitri ⊢ ( ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ ∃ 𝑧 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ ∃ 𝑧 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ↔ ∃ 𝑧 ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) )
137 102 119 136 3bitr3g ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ∃ 𝑤 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑧 ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) ) )
138 137 abbidv ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → { 𝑥 ∣ ∃ 𝑤 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } )
139 dmopab ⊢ dom { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } = { 𝑥 ∣ ∃ 𝑤 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) }
140 dmopab ⊢ dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) }
141 138 139 140 3eqtr4g ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } = dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } )
142 63 141 uneq12d ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ dom { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = ( dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) )
143 dmun ⊢ dom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ dom { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } )
144 dmun ⊢ dom ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) = ( dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ dom { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } )
145 142 143 144 3eqtr4g ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = dom ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) )
146 simpl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 )
147 146 adantr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → 𝑀 ∈ 𝑉 )
148 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 )
149 148 adantr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → 𝐸 ∈ 𝑊 )
150 48 satfvsuc ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑦 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
151 147 149 65 150 syl2an23an ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
152 151 dmeqd ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
153 simprl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → 𝑁 ∈ 𝑋 )
154 simprr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → 𝐹 ∈ 𝑌 )
155 54 satfvsuc ⊢ ( ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ∧ 𝑦 ∈ ω ) → ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) = ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) )
156 153 154 65 155 syl2an23an ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) = ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) )
157 156 dmeqd ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) = dom ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) )
158 152 157 eqeq12d ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ↔ dom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = dom ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) ) )
159 158 adantr ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ↔ dom ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑤 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑤 = { 𝑚 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) = dom ( ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ( 𝑥 = ( ( 1st ‘ 𝑎 ) ⊼𝑔 ( 1st ‘ 𝑏 ) ) ∧ 𝑧 = ( ( 𝑁 ↑m ω ) ∖ ( ( 2nd ‘ 𝑎 ) ∩ ( 2nd ‘ 𝑏 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑎 ) ∧ 𝑧 = { 𝑚 ∈ ( 𝑁 ↑m ω ) ∣ ∀ 𝑓 ∈ 𝑁 ( { ⟨ 𝑖 , 𝑓 ⟩ } ∪ ( 𝑚 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑎 ) } ) ) } ) ) )
160 145 159 mpbird ⊢ ( ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) )
161 160 ex ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) )
162 62 161 syld ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ) → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) )
163 162 ex ⊢ ( 𝑦 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) ) )
164 163 com23 ⊢ ( 𝑦 ∈ ω → ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑦 ) ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ suc 𝑦 ) ) ) )
165 6 12 18 24 60 164 finds ⊢ ( 𝑛 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) ) )
166 165 impcom ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) ∧ 𝑛 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) )
167 166 ralrimiva ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑁 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ) ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑛 ) )