Metamath Proof Explorer

Theorem trpredlem1

Description: Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subclasses of the base class. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion trpredlem1 ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 nn0suc ⊢ ( 𝑖 ∈ ω → ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) )
2 fr0g ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
3 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴
4 2 3 eqsstrdi ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ⊆ 𝐴 )
5 fveq2 ⊢ ( 𝑖 = ∅ → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) )
6 5 sseq1d ⊢ ( 𝑖 = ∅ → ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ⊆ 𝐴 ) )
7 4 6 syl5ibr ⊢ ( 𝑖 = ∅ → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ) )
8 nfcv ⊢ Ⅎ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑋 )
9 nfcv ⊢ Ⅎ 𝑎 𝑗
10 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) )
11 10 8 nfrdg ⊢ Ⅎ 𝑎 rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
12 nfcv ⊢ Ⅎ 𝑎 ω
13 11 12 nfres ⊢ Ⅎ 𝑎 ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
14 13 9 nffv ⊢ Ⅎ 𝑎 ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 )
15 nfcv ⊢ Ⅎ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 )
16 14 15 nfiun ⊢ Ⅎ 𝑎 ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 )
17 predeq3 ⊢ ( 𝑦 = 𝑒 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑒 ) )
18 17 cbviunv ⊢ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 )
19 18 mpteq2i ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) )
20 rdgeq1 ⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
21 reseq1 ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
22 19 20 21 mp2b ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
23 iuneq1 ⊢ ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → ∪ 𝑒 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑒 ) = ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) )
24 8 9 16 22 23 frsucmpt ⊢ ( ( 𝑗 ∈ ω ∧ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) = ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) )
25 iunss ⊢ ( ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ⊆ 𝐴 ↔ ∀ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ⊆ 𝐴 )
26 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑒 ) ⊆ 𝐴
27 26 a1i ⊢ ( 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → Pred ( 𝑅 , 𝐴 , 𝑒 ) ⊆ 𝐴 )
28 25 27 mprgbir ⊢ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ⊆ 𝐴
29 24 28 eqsstrdi ⊢ ( ( 𝑗 ∈ ω ∧ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 )
30 8 9 16 22 23 frsucmptn ⊢ ( ¬ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) = ∅ )
31 30 adantl ⊢ ( ( 𝑗 ∈ ω ∧ ¬ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) = ∅ )
32 0ss ⊢ ∅ ⊆ 𝐴
33 31 32 eqsstrdi ⊢ ( ( 𝑗 ∈ ω ∧ ¬ ∪ 𝑒 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) Pred ( 𝑅 , 𝐴 , 𝑒 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 )
34 29 33 pm2.61dan ⊢ ( 𝑗 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 )
35 34 adantr ⊢ ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 )
36 fveq2 ⊢ ( 𝑖 = suc 𝑗 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) )
37 36 sseq1d ⊢ ( 𝑖 = suc 𝑗 → ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 ) )
38 37 adantl ⊢ ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) → ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑗 ) ⊆ 𝐴 ) )
39 35 38 mpbird ⊢ ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
40 39 rexlimiva ⊢ ( ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
41 40 a1d ⊢ ( ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ) )
42 7 41 jaoi ⊢ ( ( 𝑖 = ∅ ∨ ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ) )
43 1 42 syl ⊢ ( 𝑖 ∈ ω → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ) )
44 nfvres ⊢ ( ¬ 𝑖 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ∅ )
45 44 32 eqsstrdi ⊢ ( ¬ 𝑖 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
46 45 a1d ⊢ ( ¬ 𝑖 ∈ ω → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ) )
47 43 46 pm2.61i ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )