Metamath Proof Explorer

Theorem tratrbVD

Description: Virtual deduction proof of tratrb . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ).
2:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr A ).
3:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
4:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. B e. A ).
5:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. y /\ y e. B ) ).
6:5,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. y ).
7:5,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. B ).
8:2,7,4,?: e121 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. A ).
9:2,6,8,?: e122 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. A ).
10:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. B e. x ).
11:6,7,10,?: e223 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. ( x e. y /\ y e. B /\ B e. x ) ).
12:11: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( B e. x -> ( x e. y /\ y e. B /\ B e. x ) ) ).
13:: |- -. ( x e. y /\ y e. B /\ B e. x )
14:12,13,?: e20 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. B e. x ).
15:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. x = B ).
16:7,15,?: e23 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. y e. x ).
17:6,16,?: e23 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. ( x e. y /\ y e. x ) ).
18:17: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x = B -> ( x e. y /\ y e. x ) ) ).
19:: |- -. ( x e. y /\ y e. x )
20:18,19,?: e20 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. x = B ).
21:3,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y e. A A. x e. A ( x e. y \/ y e. x \/ x = y ) ).
22:21,9,4,?: e121 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. x / x ]. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
23:22,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
24:4,23,?: e12 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. B \/ B e. x \/ x = B ) ).
25:14,20,24,?: e222 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. B ).
26:25: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( ( x e. y /\ y e. B ) -> x e. B ) ).
27:: |- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. y A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
28:27,?: e0a |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. y ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
29:28,26: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
30:: |- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. x A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
31:30,?: e0a |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. x ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
32:31,29: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
33:32,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr B ).
qed:33: |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion tratrbVD ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → Tr 𝐵 )

Proof

Step Hyp Ref Expression
1 hbra1 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑥 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
2 alrim3con13v ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑥 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → ∀ 𝑥 ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) ) )
3 1 2 e0a ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → ∀ 𝑥 ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) )
4 ax-5 ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝑥 ∈ 𝐴 )
5 hbra1 ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑦 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
6 4 5 hbral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
7 alrim3con13v ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → ∀ 𝑦 ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) ) )
8 6 7 e0a ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → ∀ 𝑦 ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) )
9 idn2 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    )
10 simpl ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝑦 )
11 9 10 e2 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    𝑥 ∈ 𝑦    )
12 simpr ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
13 9 12 e2 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    𝑦 ∈ 𝐵    )
14 idn3 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ,    𝐵 ∈ 𝑥    ▶    𝐵 ∈ 𝑥    )
15 pm3.2an3 ⊢ ( 𝑥 ∈ 𝑦 → ( 𝑦 ∈ 𝐵 → ( 𝐵 ∈ 𝑥 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 ) ) ) )
16 11 13 14 15 e223 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ,    𝐵 ∈ 𝑥    ▶    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 )    )
17 16 in3 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ( 𝐵 ∈ 𝑥 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 ) )    )
18 en3lp ⊢ ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 )
19 con3 ⊢ ( ( 𝐵 ∈ 𝑥 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 ) ) → ( ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝑥 ) → ¬ 𝐵 ∈ 𝑥 ) )
20 17 18 19 e20 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ¬ 𝐵 ∈ 𝑥    )
21 idn3 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ,    𝑥 = 𝐵    ▶    𝑥 = 𝐵    )
22 eleq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐵 ) )
23 22 biimprcd ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑥 = 𝐵 → 𝑦 ∈ 𝑥 ) )
24 13 21 23 e23 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ,    𝑥 = 𝐵    ▶    𝑦 ∈ 𝑥    )
25 pm3.2 ⊢ ( 𝑥 ∈ 𝑦 → ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) )
26 11 24 25 e23 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ,    𝑥 = 𝐵    ▶    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 )    )
27 26 in3 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) )    )
28 en2lp ⊢ ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 )
29 con3 ⊢ ( ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ) → ( ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ¬ 𝑥 = 𝐵 ) )
30 27 28 29 e20 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ¬ 𝑥 = 𝐵    )
31 idn1 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    )
32 simp3 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
33 31 32 e1a ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    𝐵 ∈ 𝐴    )
34 simp2 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
35 31 34 e1a ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 )    )
36 ralcom ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
37 36 biimpi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
38 35 37 e1a ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 )    )
39 simp1 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → Tr 𝐴 )
40 31 39 e1a ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    Tr 𝐴    )
41 trel ⊢ ( Tr 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
42 41 expd ⊢ ( Tr 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝐵 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
43 40 13 33 42 e121 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    𝑦 ∈ 𝐴    )
44 trel ⊢ ( Tr 𝐴 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) )
45 44 expd ⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) ) )
46 40 11 43 45 e122 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    𝑥 ∈ 𝐴    )
47 rspsbc2 ⊢ ( 𝐵 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) ) )
48 47 com13 ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ 𝐴 → [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) ) )
49 38 46 33 48 e121 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 )    )
50 equid ⊢ 𝑥 = 𝑥
51 sbceq2a ⊢ ( 𝑥 = 𝑥 → ( [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
52 50 51 ax-mp ⊢ ( [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
53 52 biimpi ⊢ ( [ 𝑥 / 𝑥 ] [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
54 49 53 e2 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 )    )
55 sbcoreleleq ⊢ ( 𝐵 ∈ 𝐴 → ( [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵 ) ) )
56 55 biimpd ⊢ ( 𝐵 ∈ 𝐴 → ( [ 𝐵 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵 ) ) )
57 33 54 56 e12 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    ( 𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵 )    )
58 3ornot23 ⊢ ( ( ¬ 𝐵 ∈ 𝑥 ∧ ¬ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐵 ) )
59 58 ex ⊢ ( ¬ 𝐵 ∈ 𝑥 → ( ¬ 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐵 ∨ 𝐵 ∈ 𝑥 ∨ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝐵 ) ) )
60 20 30 57 59 e222 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ,    ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )    ▶    𝑥 ∈ 𝐵    )
61 60 in2 ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )    )
62 8 61 gen11nv ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )    )
63 3 62 gen11nv ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )    )
64 dftr2 ⊢ ( Tr 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) )
65 64 biimpri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) → Tr 𝐵 )
66 63 65 e1a ⊢ (    ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 )    ▶    Tr 𝐵    )
67 66 in1 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ∧ 𝐵 ∈ 𝐴 ) → Tr 𝐵 )