Theorem onfrALTlem2VD 45045

Description: Virtual deduction proof of onfrALTlem2 44703. 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 44703 is onfrALTlem2VD 45045 without virtual deductions and was automatically derived from onfrALTlem2VD 45045.

1::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   )
2:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑦)   )
3:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑎   )
4::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
5::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
6:5:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
7:4:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
8:6,7:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
9:8:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
10:9:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Tr 𝑥   )
11:1:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
12:11:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ 𝑥   )
13:2:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑦   )
14:10,12,13:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑥   )
15:3,14:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑥)   )
16:13,15:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
17:16:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
18:17:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
19:18:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
20::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
21:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
22:19,21:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑎 ∩ 𝑦) = ∅   )
23:20:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
24:23:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   𝑦 ∈ 𝑎   )
25:22,24:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅), (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)   ▶   (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
26:25:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
27:26:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
28:27:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥 ) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
29::	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅   )
30:29:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
31:28,30:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
qed:31:	⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎(𝑎 ∩ 𝑦) = ∅   )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable groups:   𝑦,𝑎   𝑥,𝑦

Proof of Theorem onfrALTlem2VD

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn3 44772	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   )
2		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦)) → 𝑧 ∈ (𝑎 ∩ 𝑦))
3	1, 2	e3 44893	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑦)   )
4		inss2 4187	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∩ 𝑦) ⊆ 𝑦
5	4	sseli 3926	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ 𝑦)
6	3, 5	e3 44893	. . . . . . . . . . . 12 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑦   )
7		inss1 4186	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∩ 𝑦) ⊆ 𝑎
8	7	sseli 3926	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ 𝑎)
9	3, 8	e3 44893	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑎   )
10		idn2 44770	. . . . . . . . . . . . . . . . . 18 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   )
11		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → 𝑥 ∈ 𝑎)
12	10, 11	e2 44788	. . . . . . . . . . . . . . . . 17 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ 𝑎   )
13		idn1 44731	. . . . . . . . . . . . . . . . . 18 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
14		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ On)
15	13, 14	e1a 44784	. . . . . . . . . . . . . . . . 17 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ⊆ On   )
16		ssel 3924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ On → (𝑥 ∈ 𝑎 → 𝑥 ∈ On))
17	16	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑎 → (𝑎 ⊆ On → 𝑥 ∈ On))
18	12, 15, 17	e21 44886	. . . . . . . . . . . . . . . 16 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   𝑥 ∈ On   )
19		eloni 6324	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ On → Ord 𝑥)
20	18, 19	e2 44788	. . . . . . . . . . . . . . 15 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Ord 𝑥   )
21		ordtr 6328	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝑥 → Tr 𝑥)
22	20, 21	e2 44788	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   Tr 𝑥   )
23		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦)) → 𝑦 ∈ (𝑎 ∩ 𝑥))
24	1, 23	e3 44893	. . . . . . . . . . . . . . 15 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
25		inss2 4187	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∩ 𝑥) ⊆ 𝑥
26	25	sseli 3926	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑎 ∩ 𝑥) → 𝑦 ∈ 𝑥)
27	24, 26	e3 44893	. . . . . . . . . . . . . 14 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑦 ∈ 𝑥   )
28		trel 5210	. . . . . . . . . . . . . . 15 ⊢ (Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
29	28	expcomd 416	. . . . . . . . . . . . . 14 ⊢ (Tr 𝑥 → (𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)))
30	22, 27, 6, 29	e233 44921	. . . . . . . . . . . . 13 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ 𝑥   )
31		elin 3914	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑎 ∩ 𝑥) ↔ (𝑧 ∈ 𝑎 ∧ 𝑧 ∈ 𝑥))
32	31	simplbi2 500	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑎 → (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑎 ∩ 𝑥)))
33	9, 30, 32	e33 44890	. . . . . . . . . . . 12 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ (𝑎 ∩ 𝑥)   )
34		elin 3914	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦) ↔ (𝑧 ∈ (𝑎 ∩ 𝑥) ∧ 𝑧 ∈ 𝑦))
35	34	simplbi2com 502	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ (𝑎 ∩ 𝑥) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)))
36	6, 33, 35	e33 44890	. . . . . . . . . . 11 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) ∧ 𝑧 ∈ (𝑎 ∩ 𝑦))   ▶   𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
37	36	in3an 44768	. . . . . . . . . 10 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
38	37	gen31 44778	. . . . . . . . 9 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦))   )
39		df-ss 3915	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) ↔ ∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)))
40	39	biimpri 228	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 ∈ (𝑎 ∩ 𝑦) → 𝑧 ∈ ((𝑎 ∩ 𝑥) ∩ 𝑦)) → (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦))
41	38, 40	e3 44893	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦)   )
42		idn3 44772	. . . . . . . . 9 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
43		simpr 484	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
44	42, 43	e3 44893	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
45		sseq0 4352	. . . . . . . . 9 ⊢ (((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑎 ∩ 𝑦) = ∅)
46	45	ex 412	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑦) ⊆ ((𝑎 ∩ 𝑥) ∩ 𝑦) → (((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ → (𝑎 ∩ 𝑦) = ∅))
47	41, 44, 46	e33 44890	. . . . . . 7 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑎 ∩ 𝑦) = ∅   )
48		simpl 482	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → 𝑦 ∈ (𝑎 ∩ 𝑥))
49	42, 48	e3 44893	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   𝑦 ∈ (𝑎 ∩ 𝑥)   )
50		inss1 4186	. . . . . . . . 9 ⊢ (𝑎 ∩ 𝑥) ⊆ 𝑎
51	50	sseli 3926	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑎 ∩ 𝑥) → 𝑦 ∈ 𝑎)
52	49, 51	e3 44893	. . . . . . 7 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   𝑦 ∈ 𝑎   )
53		pm3.21 471	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑦) = ∅ → (𝑦 ∈ 𝑎 → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
54	47, 52, 53	e33 44890	. . . . . 6 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ,   (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   ▶   (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
55	54	in3 44766	. . . . 5 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
56	55	gen21 44776	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
57		exim 1835	. . . 4 ⊢ (∀𝑦((𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) → (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
58	56, 57	e2 44788	. . 3 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))   )
59		onfrALTlem3VD 45043	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅   )
60		df-rex 3058	. . . . 5 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
61	60	biimpi 216	. . . 4 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ → ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
62	59, 61	e2 44788	. . 3 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)   )
63		id 22	. . 3 ⊢ ((∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) → (∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅) → ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)))
64	58, 62, 63	e22 44828	. 2 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)   )
65		df-rex 3058	. . 3 ⊢ (∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
66	65	biimpri 228	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)
67	64, 66	e2 44788	1 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2929  ∃wrex 3057   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  Tr wtr 5202  Ord word 6313  Oncon0 6314  (   wvd2 44734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-tr 5203  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318  df-vd1 44727  df-vd2 44735  df-vd3 44747

This theorem is referenced by:  onfrALTVD  45047