Metamath Proof Explorer

Theorem suctrALT2VD

Description: Virtual deduction proof of suctrALT2 . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT2VD ( Tr 𝐴 → Tr suc 𝐴 )

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
2 sssucid ⊢ 𝐴 ⊆ suc 𝐴
3 idn1 ⊢ (    Tr 𝐴    ▶    Tr 𝐴    )
4 idn2 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    )
5 simpl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
6 4 5 e2 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    𝑧 ∈ 𝑦    )
7 idn3 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 ∈ 𝐴    ▶    𝑦 ∈ 𝐴    )
8 trel ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
9 8 expd ⊢ ( Tr 𝐴 → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) )
10 3 6 7 9 e123 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 ∈ 𝐴    ▶    𝑧 ∈ 𝐴    )
11 ssel ⊢ ( 𝐴 ⊆ suc 𝐴 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) )
12 2 10 11 e03 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 ∈ 𝐴    ▶    𝑧 ∈ suc 𝐴    )
13 12 in3 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 )    )
14 idn3 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 = 𝐴    ▶    𝑦 = 𝐴    )
15 eleq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴 ) )
16 15 biimpcd ⊢ ( 𝑧 ∈ 𝑦 → ( 𝑦 = 𝐴 → 𝑧 ∈ 𝐴 ) )
17 6 14 16 e23 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 = 𝐴    ▶    𝑧 ∈ 𝐴    )
18 2 17 11 e03 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ,    𝑦 = 𝐴    ▶    𝑧 ∈ suc 𝐴    )
19 18 in3 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 )    )
20 simpr ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
21 4 20 e2 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    𝑦 ∈ suc 𝐴    )
22 elsuci ⊢ ( 𝑦 ∈ suc 𝐴 → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
23 21 22 e2 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 )    )
24 jao ⊢ ( ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 ) ) )
25 13 19 23 24 e222 ⊢ (    Tr 𝐴    ,    ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 )    ▶    𝑧 ∈ suc 𝐴    )
26 25 in2 ⊢ (    Tr 𝐴    ▶    ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 )    )
27 26 gen12 ⊢ (    Tr 𝐴    ▶    ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 )    )
28 biimpr ⊢ ( ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) ) → ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) → Tr suc 𝐴 ) )
29 1 27 28 e01 ⊢ (    Tr 𝐴    ▶    Tr suc 𝐴    )
30 29 in1 ⊢ ( Tr 𝐴 → Tr suc 𝐴 )