Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bnj1034.1 | ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) | |
| bnj1034.2 | ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) | ||
| bnj1034.3 | ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) | ||
| bnj1034.4 | ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) | ||
| bnj1034.5 | ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) ) | ||
| bnj1034.7 | ⊢ ( 𝜁 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) | ||
| bnj1034.8 | ⊢ 𝐷 = ( ω ∖ { ∅ } ) | ||
| bnj1034.9 | ⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } | ||
| bnj1034.10 | ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → 𝑧 ∈ 𝐵 ) | ||
| Assertion | bnj1034 | ⊢ ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bnj1034.1 | ⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) | |
| 2 | bnj1034.2 | ⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) | |
| 3 | bnj1034.3 | ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) | |
| 4 | bnj1034.4 | ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) | |
| 5 | bnj1034.5 | ⊢ ( 𝜏 ↔ ( 𝐵 ∈ V ∧ TrFo ( 𝐵 , 𝐴 , 𝑅 ) ∧ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) ) | |
| 6 | bnj1034.7 | ⊢ ( 𝜁 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ ( 𝑓 ‘ 𝑖 ) ) ) | |
| 7 | bnj1034.8 | ⊢ 𝐷 = ( ω ∖ { ∅ } ) | |
| 8 | bnj1034.9 | ⊢ 𝐾 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } | |
| 9 | bnj1034.10 | ⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁 ) → 𝑧 ∈ 𝐵 ) | |
| 10 | biid | ⊢ ( 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) | |
| 11 | 1 2 3 4 5 10 6 7 8 9 | bnj1033 | ⊢ ( ( 𝜃 ∧ 𝜏 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐵 ) |