Proof of Theorem aomclem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aomclem5.f | . . . . . 6
⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} | 
| 2 |  | aomclem5.on | . . . . . . 7
⊢ (𝜑 → dom 𝑧 ∈ On) | 
| 3 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → dom 𝑧 ∈ On) | 
| 4 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → dom 𝑧 = ∪ dom 𝑧) | 
| 5 |  | aomclem5.we | . . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) | 
| 6 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) | 
| 7 | 1, 3, 4, 6 | aomclem4 43074 | . . . . 5
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → 𝐹 We (𝑅1‘dom 𝑧)) | 
| 8 |  | iftrue 4530 | . . . . . . 7
⊢ (dom
𝑧 = ∪ dom 𝑧 → if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) = 𝐹) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) = 𝐹) | 
| 10 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) →
(𝑅1‘dom 𝑧) = (𝑅1‘dom 𝑧)) | 
| 11 | 9, 10 | weeq12d 5673 | . . . . 5
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → (if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧) ↔ 𝐹 We (𝑅1‘dom 𝑧))) | 
| 12 | 7, 11 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ dom 𝑧 = ∪ dom 𝑧) → if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧)) | 
| 13 |  | aomclem5.b | . . . . . 6
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} | 
| 14 |  | aomclem5.c | . . . . . 6
⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) | 
| 15 |  | aomclem5.d | . . . . . 6
⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom
𝑧) ∖ ran 𝑎)))) | 
| 16 |  | aomclem5.e | . . . . . 6
⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩
(◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} | 
| 17 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → dom 𝑧 ∈ On) | 
| 18 |  | eloni 6393 | . . . . . . . 8
⊢ (dom
𝑧 ∈ On → Ord dom
𝑧) | 
| 19 |  | orduniorsuc 7851 | . . . . . . . 8
⊢ (Ord dom
𝑧 → (dom 𝑧 = ∪
dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧)) | 
| 20 | 2, 18, 19 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (dom 𝑧 = ∪ dom 𝑧 ∨ dom 𝑧 = suc ∪ dom 𝑧)) | 
| 21 | 20 | orcanai 1004 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → dom 𝑧 = suc ∪ dom 𝑧) | 
| 22 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) | 
| 23 |  | aomclem5.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ On) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → 𝐴 ∈ On) | 
| 25 |  | aomclem5.za | . . . . . . 7
⊢ (𝜑 → dom 𝑧 ⊆ 𝐴) | 
| 26 | 25 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → dom 𝑧 ⊆ 𝐴) | 
| 27 |  | aomclem5.y | . . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ 𝒫
(𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖
{∅}))) | 
| 28 | 27 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → ∀𝑎 ∈ 𝒫
(𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖
{∅}))) | 
| 29 | 13, 14, 15, 16, 17, 21, 22, 24, 26, 28 | aomclem3 43073 | . . . . 5
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → 𝐸 We
(𝑅1‘dom 𝑧)) | 
| 30 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
dom 𝑧 = ∪ dom 𝑧 → if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) = 𝐸) | 
| 31 | 30 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) = 𝐸) | 
| 32 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) →
(𝑅1‘dom 𝑧) = (𝑅1‘dom 𝑧)) | 
| 33 | 31, 32 | weeq12d 5673 | . . . . 5
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → (if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧) ↔ 𝐸 We (𝑅1‘dom 𝑧))) | 
| 34 | 29, 33 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ ¬ dom 𝑧 = ∪
dom 𝑧) → if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧)) | 
| 35 | 12, 34 | pm2.61dan 812 | . . 3
⊢ (𝜑 → if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧)) | 
| 36 |  | weinxp 5769 | . . 3
⊢ (if(dom
𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) We (𝑅1‘dom 𝑧) ↔ (if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) We (𝑅1‘dom 𝑧)) | 
| 37 | 35, 36 | sylib 218 | . 2
⊢ (𝜑 → (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) We (𝑅1‘dom 𝑧)) | 
| 38 |  | aomclem5.g | . . 3
⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) | 
| 39 |  | weeq1 5671 | . . 3
⊢ (𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) → (𝐺 We (𝑅1‘dom 𝑧) ↔ (if(dom 𝑧 = ∪
dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) We (𝑅1‘dom 𝑧))) | 
| 40 | 38, 39 | ax-mp 5 | . 2
⊢ (𝐺 We
(𝑅1‘dom 𝑧) ↔ (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom
𝑧) ×
(𝑅1‘dom 𝑧))) We (𝑅1‘dom 𝑧)) | 
| 41 | 37, 40 | sylibr 234 | 1
⊢ (𝜑 → 𝐺 We (𝑅1‘dom 𝑧)) |