Description: Lemma for pwfseq . Although in some ways pwfseqlem4 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection K from the set of finite sequences on an infinite set x to x . Now this alone would not be difficult to prove; this is mostly the claim of fseqen . However, what is needed for the proof is acanonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas.
If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen . The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms ( cnfcom3c ), which can be used to construct a pairing function explicitly using properties of the ordinal exponential ( infxpenc ). (Contributed by Mario Carneiro, 31-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | pwfseqlem5.g | ⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) | |
| pwfseqlem5.x | ⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 ) | ||
| pwfseqlem5.h | ⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 ) | ||
| pwfseqlem5.ps | ⊢ ( 𝜓 ↔ ( ( 𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑡 × 𝑡 ) ∧ 𝑟 We 𝑡 ) ∧ ω ≼ 𝑡 ) ) | ||
| pwfseqlem5.n | ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) | ||
| pwfseqlem5.o | ⊢ 𝑂 = OrdIso ( 𝑟 , 𝑡 ) | ||
| pwfseqlem5.t | ⊢ 𝑇 = ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) | ||
| pwfseqlem5.p | ⊢ 𝑃 = ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) | ||
| pwfseqlem5.s | ⊢ 𝑆 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑡 ↑m suc 𝑘 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑘 ) ) 𝑃 ( 𝑥 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , ( 𝑂 ‘ ∅ ) ⟩ } ) | ||
| pwfseqlem5.q | ⊢ 𝑄 = ( 𝑦 ∈ ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) ↦ ⟨ dom 𝑦 , ( ( 𝑆 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ) | ||
| pwfseqlem5.i | ⊢ 𝐼 = ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) | ||
| pwfseqlem5.k | ⊢ 𝐾 = ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) | ||
| Assertion | pwfseqlem5 | ⊢ ¬ 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pwfseqlem5.g | ⊢ ( 𝜑 → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) | |
| 2 | pwfseqlem5.x | ⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 ) | |
| 3 | pwfseqlem5.h | ⊢ ( 𝜑 → 𝐻 : ω –1-1-onto→ 𝑋 ) | |
| 4 | pwfseqlem5.ps | ⊢ ( 𝜓 ↔ ( ( 𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑡 × 𝑡 ) ∧ 𝑟 We 𝑡 ) ∧ ω ≼ 𝑡 ) ) | |
| 5 | pwfseqlem5.n | ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) | |
| 6 | pwfseqlem5.o | ⊢ 𝑂 = OrdIso ( 𝑟 , 𝑡 ) | |
| 7 | pwfseqlem5.t | ⊢ 𝑇 = ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) | |
| 8 | pwfseqlem5.p | ⊢ 𝑃 = ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) | |
| 9 | pwfseqlem5.s | ⊢ 𝑆 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( 𝑡 ↑m suc 𝑘 ) ↦ ( ( 𝑓 ‘ ( 𝑥 ↾ 𝑘 ) ) 𝑃 ( 𝑥 ‘ 𝑘 ) ) ) ) , { ⟨ ∅ , ( 𝑂 ‘ ∅ ) ⟩ } ) | |
| 10 | pwfseqlem5.q | ⊢ 𝑄 = ( 𝑦 ∈ ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) ↦ ⟨ dom 𝑦 , ( ( 𝑆 ‘ dom 𝑦 ) ‘ 𝑦 ) ⟩ ) | |
| 11 | pwfseqlem5.i | ⊢ 𝐼 = ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) | |
| 12 | pwfseqlem5.k | ⊢ 𝐾 = ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) | |
| 13 | vex | ⊢ 𝑡 ∈ V | |
| 14 | simprl3 | ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑡 × 𝑡 ) ∧ 𝑟 We 𝑡 ) ∧ ω ≼ 𝑡 ) ) → 𝑟 We 𝑡 ) | |
| 15 | 4 14 | sylan2b | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑟 We 𝑡 ) |
| 16 | 6 | oiiso | ⊢ ( ( 𝑡 ∈ V ∧ 𝑟 We 𝑡 ) → 𝑂 Isom E , 𝑟 ( dom 𝑂 , 𝑡 ) ) |
| 17 | 13 15 16 | sylancr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 Isom E , 𝑟 ( dom 𝑂 , 𝑡 ) ) |
| 18 | isof1o | ⊢ ( 𝑂 Isom E , 𝑟 ( dom 𝑂 , 𝑡 ) → 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ) | |
| 19 | 17 18 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ) |
| 20 | cardom | ⊢ ( card ‘ ω ) = ω | |
| 21 | simprr | ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑡 × 𝑡 ) ∧ 𝑟 We 𝑡 ) ∧ ω ≼ 𝑡 ) ) → ω ≼ 𝑡 ) | |
| 22 | 4 21 | sylan2b | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ω ≼ 𝑡 ) |
| 23 | 6 | oien | ⊢ ( ( 𝑡 ∈ V ∧ 𝑟 We 𝑡 ) → dom 𝑂 ≈ 𝑡 ) |
| 24 | 13 15 23 | sylancr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑂 ≈ 𝑡 ) |
| 25 | 24 | ensymd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑡 ≈ dom 𝑂 ) |
| 26 | domentr | ⊢ ( ( ω ≼ 𝑡 ∧ 𝑡 ≈ dom 𝑂 ) → ω ≼ dom 𝑂 ) | |
| 27 | 22 25 26 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ω ≼ dom 𝑂 ) |
| 28 | omelon | ⊢ ω ∈ On | |
| 29 | onenon | ⊢ ( ω ∈ On → ω ∈ dom card ) | |
| 30 | 28 29 | ax-mp | ⊢ ω ∈ dom card |
| 31 | 6 | oion | ⊢ ( 𝑡 ∈ V → dom 𝑂 ∈ On ) |
| 32 | 31 | elv | ⊢ dom 𝑂 ∈ On |
| 33 | onenon | ⊢ ( dom 𝑂 ∈ On → dom 𝑂 ∈ dom card ) | |
| 34 | 32 33 | mp1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑂 ∈ dom card ) |
| 35 | carddom2 | ⊢ ( ( ω ∈ dom card ∧ dom 𝑂 ∈ dom card ) → ( ( card ‘ ω ) ⊆ ( card ‘ dom 𝑂 ) ↔ ω ≼ dom 𝑂 ) ) | |
| 36 | 30 34 35 | sylancr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( card ‘ ω ) ⊆ ( card ‘ dom 𝑂 ) ↔ ω ≼ dom 𝑂 ) ) |
| 37 | 27 36 | mpbird | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( card ‘ ω ) ⊆ ( card ‘ dom 𝑂 ) ) |
| 38 | 20 37 | eqsstrrid | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ω ⊆ ( card ‘ dom 𝑂 ) ) |
| 39 | cardonle | ⊢ ( dom 𝑂 ∈ On → ( card ‘ dom 𝑂 ) ⊆ dom 𝑂 ) | |
| 40 | 32 39 | mp1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( card ‘ dom 𝑂 ) ⊆ dom 𝑂 ) |
| 41 | 38 40 | sstrd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ω ⊆ dom 𝑂 ) |
| 42 | sseq2 | ⊢ ( 𝑏 = dom 𝑂 → ( ω ⊆ 𝑏 ↔ ω ⊆ dom 𝑂 ) ) | |
| 43 | fveq2 | ⊢ ( 𝑏 = dom 𝑂 → ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ dom 𝑂 ) ) | |
| 44 | f1oeq1 | ⊢ ( ( 𝑁 ‘ 𝑏 ) = ( 𝑁 ‘ dom 𝑂 ) → ( ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑁 ‘ dom 𝑂 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) | |
| 45 | 43 44 | syl | ⊢ ( 𝑏 = dom 𝑂 → ( ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑁 ‘ dom 𝑂 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) |
| 46 | xpeq12 | ⊢ ( ( 𝑏 = dom 𝑂 ∧ 𝑏 = dom 𝑂 ) → ( 𝑏 × 𝑏 ) = ( dom 𝑂 × dom 𝑂 ) ) | |
| 47 | 46 | anidms | ⊢ ( 𝑏 = dom 𝑂 → ( 𝑏 × 𝑏 ) = ( dom 𝑂 × dom 𝑂 ) ) |
| 48 | 47 | f1oeq2d | ⊢ ( 𝑏 = dom 𝑂 → ( ( 𝑁 ‘ dom 𝑂 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ 𝑏 ) ) |
| 49 | f1oeq3 | ⊢ ( 𝑏 = dom 𝑂 → ( ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ 𝑏 ↔ ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) ) | |
| 50 | 45 48 49 | 3bitrd | ⊢ ( 𝑏 = dom 𝑂 → ( ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) ) |
| 51 | 42 50 | imbi12d | ⊢ ( 𝑏 = dom 𝑂 → ( ( ω ⊆ 𝑏 → ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ( ω ⊆ dom 𝑂 → ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) ) ) |
| 52 | 5 | adantr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑏 ∈ ( har ‘ 𝒫 𝐴 ) ( ω ⊆ 𝑏 → ( 𝑁 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) |
| 53 | 32 | a1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑂 ∈ On ) |
| 54 | 1 | adantr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) |
| 55 | omex | ⊢ ω ∈ V | |
| 56 | ovex | ⊢ ( 𝐴 ↑m 𝑛 ) ∈ V | |
| 57 | 55 56 | iunex | ⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V |
| 58 | f1dmex | ⊢ ( ( 𝐺 : 𝒫 𝐴 –1-1→ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V ) → 𝒫 𝐴 ∈ V ) | |
| 59 | 54 57 58 | sylancl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝒫 𝐴 ∈ V ) |
| 60 | pwexb | ⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V ) | |
| 61 | 59 60 | sylibr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ V ) |
| 62 | simprl1 | ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑡 × 𝑡 ) ∧ 𝑟 We 𝑡 ) ∧ ω ≼ 𝑡 ) ) → 𝑡 ⊆ 𝐴 ) | |
| 63 | 4 62 | sylan2b | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑡 ⊆ 𝐴 ) |
| 64 | ssdomg | ⊢ ( 𝐴 ∈ V → ( 𝑡 ⊆ 𝐴 → 𝑡 ≼ 𝐴 ) ) | |
| 65 | 61 63 64 | sylc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑡 ≼ 𝐴 ) |
| 66 | canth2g | ⊢ ( 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴 ) | |
| 67 | sdomdom | ⊢ ( 𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴 ) | |
| 68 | 61 66 67 | 3syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ≼ 𝒫 𝐴 ) |
| 69 | domtr | ⊢ ( ( 𝑡 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐴 ) → 𝑡 ≼ 𝒫 𝐴 ) | |
| 70 | 65 68 69 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑡 ≼ 𝒫 𝐴 ) |
| 71 | endomtr | ⊢ ( ( dom 𝑂 ≈ 𝑡 ∧ 𝑡 ≼ 𝒫 𝐴 ) → dom 𝑂 ≼ 𝒫 𝐴 ) | |
| 72 | 24 70 71 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑂 ≼ 𝒫 𝐴 ) |
| 73 | elharval | ⊢ ( dom 𝑂 ∈ ( har ‘ 𝒫 𝐴 ) ↔ ( dom 𝑂 ∈ On ∧ dom 𝑂 ≼ 𝒫 𝐴 ) ) | |
| 74 | 53 72 73 | sylanbrc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑂 ∈ ( har ‘ 𝒫 𝐴 ) ) |
| 75 | 51 52 74 | rspcdva | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ω ⊆ dom 𝑂 → ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) ) |
| 76 | 41 75 | mpd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) |
| 77 | f1oco | ⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ∧ ( 𝑁 ‘ dom 𝑂 ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ dom 𝑂 ) → ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ 𝑡 ) | |
| 78 | 19 76 77 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ 𝑡 ) |
| 79 | f1of | ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 → 𝑂 : dom 𝑂 ⟶ 𝑡 ) | |
| 80 | 19 79 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 : dom 𝑂 ⟶ 𝑡 ) |
| 81 | 80 | feqmptd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 = ( 𝑢 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑢 ) ) ) |
| 82 | f1oeq1 | ⊢ ( 𝑂 = ( 𝑢 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑢 ) ) → ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ↔ ( 𝑢 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑢 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) ) | |
| 83 | 81 82 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ↔ ( 𝑢 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑢 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) ) |
| 84 | 19 83 | mpbid | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑢 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑢 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) |
| 85 | 80 | feqmptd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 = ( 𝑣 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑣 ) ) ) |
| 86 | f1oeq1 | ⊢ ( 𝑂 = ( 𝑣 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑣 ) ) → ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ↔ ( 𝑣 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑣 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) ) | |
| 87 | 85 86 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 ↔ ( 𝑣 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑣 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) ) |
| 88 | 19 87 | mpbid | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑣 ∈ dom 𝑂 ↦ ( 𝑂 ‘ 𝑣 ) ) : dom 𝑂 –1-1-onto→ 𝑡 ) |
| 89 | 84 88 | xpf1o | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ) |
| 90 | f1oeq1 | ⊢ ( 𝑇 = ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) → ( 𝑇 : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ↔ ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ) ) | |
| 91 | 7 90 | ax-mp | ⊢ ( 𝑇 : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ↔ ( 𝑢 ∈ dom 𝑂 , 𝑣 ∈ dom 𝑂 ↦ ⟨ ( 𝑂 ‘ 𝑢 ) , ( 𝑂 ‘ 𝑣 ) ⟩ ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ) |
| 92 | 89 91 | sylibr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) ) |
| 93 | f1ocnv | ⊢ ( 𝑇 : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ ( 𝑡 × 𝑡 ) → ◡ 𝑇 : ( 𝑡 × 𝑡 ) –1-1-onto→ ( dom 𝑂 × dom 𝑂 ) ) | |
| 94 | 92 93 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ◡ 𝑇 : ( 𝑡 × 𝑡 ) –1-1-onto→ ( dom 𝑂 × dom 𝑂 ) ) |
| 95 | f1oco | ⊢ ( ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) : ( dom 𝑂 × dom 𝑂 ) –1-1-onto→ 𝑡 ∧ ◡ 𝑇 : ( 𝑡 × 𝑡 ) –1-1-onto→ ( dom 𝑂 × dom 𝑂 ) ) → ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ) | |
| 96 | 78 94 95 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ) |
| 97 | f1oeq1 | ⊢ ( 𝑃 = ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) → ( 𝑃 : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ↔ ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ) ) | |
| 98 | 8 97 | ax-mp | ⊢ ( 𝑃 : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ↔ ( ( 𝑂 ∘ ( 𝑁 ‘ dom 𝑂 ) ) ∘ ◡ 𝑇 ) : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ) |
| 99 | 96 98 | sylibr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑃 : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 ) |
| 100 | f1of1 | ⊢ ( 𝑃 : ( 𝑡 × 𝑡 ) –1-1-onto→ 𝑡 → 𝑃 : ( 𝑡 × 𝑡 ) –1-1→ 𝑡 ) | |
| 101 | 99 100 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑃 : ( 𝑡 × 𝑡 ) –1-1→ 𝑡 ) |
| 102 | f1of1 | ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ 𝑡 → 𝑂 : dom 𝑂 –1-1→ 𝑡 ) | |
| 103 | 19 102 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑂 : dom 𝑂 –1-1→ 𝑡 ) |
| 104 | f1ssres | ⊢ ( ( 𝑂 : dom 𝑂 –1-1→ 𝑡 ∧ ω ⊆ dom 𝑂 ) → ( 𝑂 ↾ ω ) : ω –1-1→ 𝑡 ) | |
| 105 | 103 41 104 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 ↾ ω ) : ω –1-1→ 𝑡 ) |
| 106 | f1f1orn | ⊢ ( ( 𝑂 ↾ ω ) : ω –1-1→ 𝑡 → ( 𝑂 ↾ ω ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ) | |
| 107 | 105 106 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 ↾ ω ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ) |
| 108 | 80 41 | feqresmpt | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 ↾ ω ) = ( 𝑥 ∈ ω ↦ ( 𝑂 ‘ 𝑥 ) ) ) |
| 109 | f1oeq1 | ⊢ ( ( 𝑂 ↾ ω ) = ( 𝑥 ∈ ω ↦ ( 𝑂 ‘ 𝑥 ) ) → ( ( 𝑂 ↾ ω ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ↔ ( 𝑥 ∈ ω ↦ ( 𝑂 ‘ 𝑥 ) ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ) ) | |
| 110 | 108 109 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑂 ↾ ω ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ↔ ( 𝑥 ∈ ω ↦ ( 𝑂 ‘ 𝑥 ) ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ) ) |
| 111 | 107 110 | mpbid | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 ∈ ω ↦ ( 𝑂 ‘ 𝑥 ) ) : ω –1-1-onto→ ran ( 𝑂 ↾ ω ) ) |
| 112 | mptresid | ⊢ ( I ↾ 𝑡 ) = ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) | |
| 113 | 112 | eqcomi | ⊢ ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) = ( I ↾ 𝑡 ) |
| 114 | f1oi | ⊢ ( I ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑡 | |
| 115 | f1oeq1 | ⊢ ( ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) = ( I ↾ 𝑡 ) → ( ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) : 𝑡 –1-1-onto→ 𝑡 ↔ ( I ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑡 ) ) | |
| 116 | 114 115 | mpbiri | ⊢ ( ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) = ( I ↾ 𝑡 ) → ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) : 𝑡 –1-1-onto→ 𝑡 ) |
| 117 | 113 116 | mp1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑦 ∈ 𝑡 ↦ 𝑦 ) : 𝑡 –1-1-onto→ 𝑡 ) |
| 118 | 111 117 | xpf1o | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) |
| 119 | f1oeq1 | ⊢ ( 𝐼 = ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) → ( 𝐼 : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ↔ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) ) | |
| 120 | 11 119 | ax-mp | ⊢ ( 𝐼 : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ↔ ( 𝑥 ∈ ω , 𝑦 ∈ 𝑡 ↦ ⟨ ( 𝑂 ‘ 𝑥 ) , 𝑦 ⟩ ) : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) |
| 121 | 118 120 | sylibr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) |
| 122 | f1of1 | ⊢ ( 𝐼 : ( ω × 𝑡 ) –1-1-onto→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) → 𝐼 : ( ω × 𝑡 ) –1-1→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) | |
| 123 | 121 122 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 : ( ω × 𝑡 ) –1-1→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ) |
| 124 | f1f | ⊢ ( ( 𝑂 ↾ ω ) : ω –1-1→ 𝑡 → ( 𝑂 ↾ ω ) : ω ⟶ 𝑡 ) | |
| 125 | frn | ⊢ ( ( 𝑂 ↾ ω ) : ω ⟶ 𝑡 → ran ( 𝑂 ↾ ω ) ⊆ 𝑡 ) | |
| 126 | xpss1 | ⊢ ( ran ( 𝑂 ↾ ω ) ⊆ 𝑡 → ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ⊆ ( 𝑡 × 𝑡 ) ) | |
| 127 | 105 124 125 126 | 4syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ⊆ ( 𝑡 × 𝑡 ) ) |
| 128 | f1ss | ⊢ ( ( 𝐼 : ( ω × 𝑡 ) –1-1→ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ∧ ( ran ( 𝑂 ↾ ω ) × 𝑡 ) ⊆ ( 𝑡 × 𝑡 ) ) → 𝐼 : ( ω × 𝑡 ) –1-1→ ( 𝑡 × 𝑡 ) ) | |
| 129 | 123 127 128 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 : ( ω × 𝑡 ) –1-1→ ( 𝑡 × 𝑡 ) ) |
| 130 | f1co | ⊢ ( ( 𝑃 : ( 𝑡 × 𝑡 ) –1-1→ 𝑡 ∧ 𝐼 : ( ω × 𝑡 ) –1-1→ ( 𝑡 × 𝑡 ) ) → ( 𝑃 ∘ 𝐼 ) : ( ω × 𝑡 ) –1-1→ 𝑡 ) | |
| 131 | 101 129 130 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑃 ∘ 𝐼 ) : ( ω × 𝑡 ) –1-1→ 𝑡 ) |
| 132 | 13 | a1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑡 ∈ V ) |
| 133 | peano1 | ⊢ ∅ ∈ ω | |
| 134 | 133 | a1i | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∅ ∈ ω ) |
| 135 | 41 134 | sseldd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∅ ∈ dom 𝑂 ) |
| 136 | 80 135 | ffvelrnd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑂 ‘ ∅ ) ∈ 𝑡 ) |
| 137 | 132 136 99 9 10 | fseqenlem2 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑄 : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ ( ω × 𝑡 ) ) |
| 138 | f1co | ⊢ ( ( ( 𝑃 ∘ 𝐼 ) : ( ω × 𝑡 ) –1-1→ 𝑡 ∧ 𝑄 : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ ( ω × 𝑡 ) ) → ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ) | |
| 139 | 131 137 138 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ) |
| 140 | f1eq1 | ⊢ ( 𝐾 = ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) → ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ↔ ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ) ) | |
| 141 | 12 140 | ax-mp | ⊢ ( 𝐾 : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ↔ ( ( 𝑃 ∘ 𝐼 ) ∘ 𝑄 ) : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ) |
| 142 | 139 141 | sylibr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 : ∪ 𝑛 ∈ ω ( 𝑡 ↑m 𝑛 ) –1-1→ 𝑡 ) |
| 143 | eqid | ⊢ ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) = ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) | |
| 144 | eqid | ⊢ ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) = ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) | |
| 145 | eqid | ⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ ( 𝑐 × 𝑐 ) ) ∧ ( 𝑑 We 𝑐 ∧ ∀ 𝑚 ∈ 𝑐 [ ( ◡ 𝑑 “ { 𝑚 } ) / 𝑗 ] ( 𝑗 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑑 ∩ ( 𝑗 × 𝑗 ) ) ) = 𝑚 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ ( 𝑐 × 𝑐 ) ) ∧ ( 𝑑 We 𝑐 ∧ ∀ 𝑚 ∈ 𝑐 [ ( ◡ 𝑑 “ { 𝑚 } ) / 𝑗 ] ( 𝑗 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑑 ∩ ( 𝑗 × 𝑗 ) ) ) = 𝑚 ) ) } | |
| 146 | 145 | fpwwe2cbv | ⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ ( 𝑐 × 𝑐 ) ) ∧ ( 𝑑 We 𝑐 ∧ ∀ 𝑚 ∈ 𝑐 [ ( ◡ 𝑑 “ { 𝑚 } ) / 𝑗 ] ( 𝑗 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑑 ∩ ( 𝑗 × 𝑗 ) ) ) = 𝑚 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑏 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑏 } ) / 𝑤 ] ( 𝑤 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑠 ∩ ( 𝑤 × 𝑤 ) ) ) = 𝑏 ) ) } |
| 147 | eqid | ⊢ ∪ dom { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ ( 𝑐 × 𝑐 ) ) ∧ ( 𝑑 We 𝑐 ∧ ∀ 𝑚 ∈ 𝑐 [ ( ◡ 𝑑 “ { 𝑚 } ) / 𝑗 ] ( 𝑗 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑑 ∩ ( 𝑗 × 𝑗 ) ) ) = 𝑚 ) ) } = ∪ dom { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ⊆ 𝐴 ∧ 𝑑 ⊆ ( 𝑐 × 𝑐 ) ) ∧ ( 𝑑 We 𝑐 ∧ ∀ 𝑚 ∈ 𝑐 [ ( ◡ 𝑑 “ { 𝑚 } ) / 𝑗 ] ( 𝑗 ( 𝑡 ∈ V , 𝑟 ∈ V ↦ if ( 𝑡 ∈ Fin , ( 𝐻 ‘ ( card ‘ 𝑡 ) ) , ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ ∩ { 𝑧 ∈ ω ∣ ¬ ( ( 𝐺 ‘ { 𝑖 ∈ 𝑡 ∣ ( ( ◡ 𝐾 ‘ 𝑖 ) ∈ ran 𝐺 ∧ ¬ 𝑖 ∈ ( ◡ 𝐺 ‘ ( ◡ 𝐾 ‘ 𝑖 ) ) ) } ) ‘ 𝑧 ) ∈ 𝑡 } ) ) ) ( 𝑑 ∩ ( 𝑗 × 𝑗 ) ) ) = 𝑚 ) ) } | |
| 148 | 1 2 3 4 142 143 144 146 147 | pwfseqlem4 | ⊢ ¬ 𝜑 |