Metamath Proof Explorer

Theorem opsrtoslem2

Description: Lemma for opsrtos . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrso.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
opsrtoslem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrtoslem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
opsrtoslem.q ⊢ < = ( lt ‘ 𝑅 )
opsrtoslem.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
opsrtoslem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
opsrtoslem.ps ⊢ ( 𝜓 ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
opsrtoslem.l ⊢ ≤ = ( le ‘ 𝑂 )
Assertion opsrtoslem2 ( 𝜑 → 𝑂 ∈ Toset )

Proof

Step Hyp Ref Expression
1 opsrso.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
4 opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
6 opsrtoslem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
7 opsrtoslem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
8 opsrtoslem.q ⊢ < = ( lt ‘ 𝑅 )
9 opsrtoslem.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
10 opsrtoslem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 opsrtoslem.ps ⊢ ( 𝜓 ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
12 opsrtoslem.l ⊢ ≤ = ( le ‘ 𝑂 )
13 2 2 xpexd ⊢ ( 𝜑 → ( 𝐼 × 𝐼 ) ∈ V )
14 13 4 ssexd ⊢ ( 𝜑 → 𝑇 ∈ V )
15 9 10 2 14 5 ltbwe ⊢ ( 𝜑 → 𝐶 We 𝐷 )
16 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 eqid ⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
18 16 17 8 tosso ⊢ ( 𝑅 ∈ Toset → ( 𝑅 ∈ Toset ↔ ( < Or ( Base ‘ 𝑅 ) ∧ ( I ↾ ( Base ‘ 𝑅 ) ) ⊆ ( le ‘ 𝑅 ) ) ) )
19 18 ibi ⊢ ( 𝑅 ∈ Toset → ( < Or ( Base ‘ 𝑅 ) ∧ ( I ↾ ( Base ‘ 𝑅 ) ) ⊆ ( le ‘ 𝑅 ) ) )
20 3 19 syl ⊢ ( 𝜑 → ( < Or ( Base ‘ 𝑅 ) ∧ ( I ↾ ( Base ‘ 𝑅 ) ) ⊆ ( le ‘ 𝑅 ) ) )
21 20 simpld ⊢ ( 𝜑 → < Or ( Base ‘ 𝑅 ) )
22 11 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
23 22 wemapso ⊢ ( ( 𝐶 We 𝐷 ∧ < Or ( Base ‘ 𝑅 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
24 15 21 23 syl2anc ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
25 6 16 10 7 2 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
26 soeq2 ⊢ ( 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or 𝐵 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ) )
27 25 26 syl ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or 𝐵 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ) )
28 24 27 mpbird ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or 𝐵 )
29 soinxp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } Or 𝐵 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 )
30 28 29 sylib ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 )
31 1 fvexi ⊢ 𝑂 ∈ V
32 eqid ⊢ ( lt ‘ 𝑂 ) = ( lt ‘ 𝑂 )
33 12 32 pltfval ⊢ ( 𝑂 ∈ V → ( lt ‘ 𝑂 ) = ( ≤ ∖ I ) )
34 31 33 ax-mp ⊢ ( lt ‘ 𝑂 ) = ( ≤ ∖ I )
35 difundir ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) ∖ I ) = ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) ∪ ( ( I ↾ 𝐵 ) ∖ I ) )
36 resss ⊢ ( I ↾ 𝐵 ) ⊆ I
37 ssdif0 ⊢ ( ( I ↾ 𝐵 ) ⊆ I ↔ ( ( I ↾ 𝐵 ) ∖ I ) = ∅ )
38 36 37 mpbi ⊢ ( ( I ↾ 𝐵 ) ∖ I ) = ∅
39 38 uneq2i ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) ∪ ( ( I ↾ 𝐵 ) ∖ I ) ) = ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) ∪ ∅ )
40 un0 ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) ∪ ∅ ) = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I )
41 35 39 40 3eqtri ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) ∖ I ) = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I )
42 1 2 3 4 5 6 7 8 9 10 11 12 opsrtoslem1 ⊢ ( 𝜑 → ≤ = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) )
43 42 difeq1d ⊢ ( 𝜑 → ( ≤ ∖ I ) = ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) ∖ I ) )
44 relinxp ⊢ Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) )
45 44 a1i ⊢ ( 𝜑 → Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) )
46 df-br ⊢ ( 𝑎 I 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ I )
47 vex ⊢ 𝑏 ∈ V
48 47 ideq ⊢ ( 𝑎 I 𝑏 ↔ 𝑎 = 𝑏 )
49 46 48 bitr3i ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ I ↔ 𝑎 = 𝑏 )
50 brin ⊢ ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ↔ ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } 𝑎 ∧ 𝑎 ( 𝐵 × 𝐵 ) 𝑎 ) )
51 50 simprbi ⊢ ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 → 𝑎 ( 𝐵 × 𝐵 ) 𝑎 )
52 brxp ⊢ ( 𝑎 ( 𝐵 × 𝐵 ) 𝑎 ↔ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) )
53 52 simprbi ⊢ ( 𝑎 ( 𝐵 × 𝐵 ) 𝑎 → 𝑎 ∈ 𝐵 )
54 51 53 syl ⊢ ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 → 𝑎 ∈ 𝐵 )
55 sonr ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ¬ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 )
56 55 ex ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 → ( 𝑎 ∈ 𝐵 → ¬ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ) )
57 30 54 56 syl2im ⊢ ( 𝜑 → ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 → ¬ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ) )
58 57 pm2.01d ⊢ ( 𝜑 → ¬ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 )
59 breq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ↔ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑏 ) )
60 df-br ⊢ ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) )
61 59 60 bitrdi ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ) )
62 61 notbid ⊢ ( 𝑎 = 𝑏 → ( ¬ 𝑎 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) 𝑎 ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ) )
63 58 62 syl5ibcom ⊢ ( 𝜑 → ( 𝑎 = 𝑏 → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ) )
64 49 63 syl5bi ⊢ ( 𝜑 → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ I → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ) )
65 64 con2d ⊢ ( 𝜑 → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) → ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ I ) )
66 opex ⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
67 eldif ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( V ∖ I ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ V ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ I ) )
68 66 67 mpbiran ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( V ∖ I ) ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ I )
69 65 68 syl6ibr ⊢ ( 𝜑 → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( V ∖ I ) ) )
70 45 69 relssdv ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ⊆ ( V ∖ I ) )
71 disj2 ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∩ I ) = ∅ ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ⊆ ( V ∖ I ) )
72 70 71 sylibr ⊢ ( 𝜑 → ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∩ I ) = ∅ )
73 disj3 ⊢ ( ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∩ I ) = ∅ ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) )
74 72 73 sylib ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) = ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∖ I ) )
75 41 43 74 3eqtr4a ⊢ ( 𝜑 → ( ≤ ∖ I ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) )
76 34 75 syl5eq ⊢ ( 𝜑 → ( lt ‘ 𝑂 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) )
77 soeq1 ⊢ ( ( lt ‘ 𝑂 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) → ( ( lt ‘ 𝑂 ) Or 𝐵 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 ) )
78 76 77 syl ⊢ ( 𝜑 → ( ( lt ‘ 𝑂 ) Or 𝐵 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) Or 𝐵 ) )
79 30 78 mpbird ⊢ ( 𝜑 → ( lt ‘ 𝑂 ) Or 𝐵 )
80 6 1 4 opsrbas ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑂 ) )
81 7 80 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
82 soeq2 ⊢ ( 𝐵 = ( Base ‘ 𝑂 ) → ( ( lt ‘ 𝑂 ) Or 𝐵 ↔ ( lt ‘ 𝑂 ) Or ( Base ‘ 𝑂 ) ) )
83 81 82 syl ⊢ ( 𝜑 → ( ( lt ‘ 𝑂 ) Or 𝐵 ↔ ( lt ‘ 𝑂 ) Or ( Base ‘ 𝑂 ) ) )
84 79 83 mpbid ⊢ ( 𝜑 → ( lt ‘ 𝑂 ) Or ( Base ‘ 𝑂 ) )
85 81 reseq2d ⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( I ↾ ( Base ‘ 𝑂 ) ) )
86 ssun2 ⊢ ( I ↾ 𝐵 ) ⊆ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) )
87 85 86 eqsstrrdi ⊢ ( 𝜑 → ( I ↾ ( Base ‘ 𝑂 ) ) ⊆ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∩ ( 𝐵 × 𝐵 ) ) ∪ ( I ↾ 𝐵 ) ) )
88 87 42 sseqtrrd ⊢ ( 𝜑 → ( I ↾ ( Base ‘ 𝑂 ) ) ⊆ ≤ )
89 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
90 89 12 32 tosso ⊢ ( 𝑂 ∈ V → ( 𝑂 ∈ Toset ↔ ( ( lt ‘ 𝑂 ) Or ( Base ‘ 𝑂 ) ∧ ( I ↾ ( Base ‘ 𝑂 ) ) ⊆ ≤ ) ) )
91 31 90 ax-mp ⊢ ( 𝑂 ∈ Toset ↔ ( ( lt ‘ 𝑂 ) Or ( Base ‘ 𝑂 ) ∧ ( I ↾ ( Base ‘ 𝑂 ) ) ⊆ ≤ ) )
92 84 88 91 sylanbrc ⊢ ( 𝜑 → 𝑂 ∈ Toset )