Metamath Proof Explorer

Theorem onfrALTlem2VD

Description: Virtual deduction proof of onfrALTlem2 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem2 is onfrALTlem2VD without virtual deductions and was automatically derived from onfrALTlem2VD .

1:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ).
2:1: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i y ) ).
3:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. a ).
4:: |- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
5:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
6:5: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
7:4: |- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
8:6,7: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
9:8: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
10:9: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Tr x ).
11:1: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. ( a i^i x ) ).
12:11: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. x ).
13:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. y ).
14:10,12,13: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. x ).
15:3,14: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i x ) ).
16:13,15: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( ( a i^i x ) i^i y ) ).
17:16: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
18:17: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
19:18: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) C_ ( ( a i^i x ) i^i y ) ).
20:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
21:20: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( ( a i^i x ) i^i y ) = (/) ).
22:19,21: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) = (/) ).
23:20: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. ( a i^i x ) ).
24:23: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. a ).
25:22,24: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. a /\ ( a i^i y ) = (/) ) ).
26:25: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
27:26: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. y ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
28:27: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ).
29:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ).
30:29: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
31:28,30: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
qed:31: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem2VD (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅    )

Proof

Step Hyp Ref Expression
1 idn3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    )
2 simpr ⊢ ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )
3 1 2 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ ( 𝑎 ∩ 𝑦 )    )
4 inss2 ⊢ ( 𝑎 ∩ 𝑦 ) ⊆ 𝑦
5 4 sseli ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ 𝑦 )
6 3 5 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ 𝑦    )
7 inss1 ⊢ ( 𝑎 ∩ 𝑦 ) ⊆ 𝑎
8 7 sseli ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ 𝑎 )
9 3 8 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ 𝑎    )
10 idn2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    )
11 simpl ⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ 𝑎 )
12 10 11 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    𝑥 ∈ 𝑎    )
13 idn1 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ▶    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    )
14 simpl ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ On )
15 13 14 e1a ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ▶    𝑎 ⊆ On    )
16 ssel ⊢ ( 𝑎 ⊆ On → ( 𝑥 ∈ 𝑎 → 𝑥 ∈ On ) )
17 16 com12 ⊢ ( 𝑥 ∈ 𝑎 → ( 𝑎 ⊆ On → 𝑥 ∈ On ) )
18 12 15 17 e21 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    𝑥 ∈ On    )
19 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
20 18 19 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    Ord 𝑥    )
21 ordtr ⊢ ( Ord 𝑥 → Tr 𝑥 )
22 20 21 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    Tr 𝑥    )
23 simpll ⊢ ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) )
24 1 23 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑦 ∈ ( 𝑎 ∩ 𝑥 )    )
25 inss2 ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥
26 25 sseli ⊢ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑦 ∈ 𝑥 )
27 24 26 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑦 ∈ 𝑥    )
28 trel ⊢ ( Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
29 28 expcomd ⊢ ( Tr 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
30 22 27 6 29 e233 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ 𝑥    )
31 elin ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑧 ∈ 𝑎 ∧ 𝑧 ∈ 𝑥 ) )
32 31 simplbi2 ⊢ ( 𝑧 ∈ 𝑎 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ) )
33 9 30 32 e33 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ ( 𝑎 ∩ 𝑥 )    )
34 elin ⊢ ( 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ↔ ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ∧ 𝑧 ∈ 𝑦 ) )
35 34 simplbi2com ⊢ ( 𝑧 ∈ 𝑦 → ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) )
36 6 33 35 e33 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )    ▶    𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 )    )
37 36 in3an ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) )    )
38 37 gen31 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) )    )
39 dfss2 ⊢ ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) )
40 39 biimpri ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) → ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) )
41 38 40 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 )    )
42 idn3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    )
43 simpr ⊢ ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
44 42 43 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅    )
45 sseq0 ⊢ ( ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑎 ∩ 𝑦 ) = ∅ )
46 45 ex ⊢ ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) → ( ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ → ( 𝑎 ∩ 𝑦 ) = ∅ ) )
47 41 44 46 e33 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( 𝑎 ∩ 𝑦 ) = ∅    )
48 simpl ⊢ ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) )
49 42 48 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    𝑦 ∈ ( 𝑎 ∩ 𝑥 )    )
50 inss1 ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑎
51 50 sseli ⊢ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑦 ∈ 𝑎 )
52 49 51 e3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    𝑦 ∈ 𝑎    )
53 pm3.21 ⊢ ( ( 𝑎 ∩ 𝑦 ) = ∅ → ( 𝑦 ∈ 𝑎 → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
54 47 52 53 e33 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ,    ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    ▶    ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ )    )
55 54 in3 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )    )
56 55 gen21 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∀ 𝑦 ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )    )
57 exim ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) → ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
58 56 57 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )    )
59 onfrALTlem3VD ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅    )
60 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
61 60 biimpi ⊢ ( ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ → ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
62 59 61 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    )
63 id ⊢ ( ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) → ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
64 58 62 63 e22 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ )    )
65 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
66 65 biimpri ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ )
67 64 66 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅    )