Metamath Proof Explorer

Theorem onvf1odlem1

Description: Lemma for onvf1od . (Contributed by BTernaryTau, 2-Dec-2025)

Ref Expression
Assertion onvf1odlem1 ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 nvel ⊢ ¬ V ∈ 𝑉
2 eleq1 ⊢ ( V = 𝐴 → ( V ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
3 2 eqcoms ⊢ ( 𝐴 = V → ( V ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
4 1 3 mtbii ⊢ ( 𝐴 = V → ¬ 𝐴 ∈ 𝑉 )
5 4 con2i ⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝐴 = V )
6 eqv ⊢ ( 𝐴 = V ↔ ∀ 𝑦 𝑦 ∈ 𝐴 )
7 alex ⊢ ( ∀ 𝑦 𝑦 ∈ 𝐴 ↔ ¬ ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 )
8 6 7 bitri ⊢ ( 𝐴 = V ↔ ¬ ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 )
9 8 con2bii ⊢ ( ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 ↔ ¬ 𝐴 = V )
10 5 9 sylibr ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 )
11 ax-1 ⊢ ( ¬ 𝑦 ∈ 𝐴 → ( 𝑥 ∈ On → ¬ 𝑦 ∈ 𝐴 ) )
12 11 ralrimiv ⊢ ( ¬ 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 )
13 12 eximi ⊢ ( ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 → ∃ 𝑦 ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 )
14 rexv ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑦 ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 )
15 13 14 sylibr ⊢ ( ∃ 𝑦 ¬ 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ V ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 )
16 tz9.13g ⊢ ( 𝑦 ∈ V → ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
17 16 rgen ⊢ ∀ 𝑦 ∈ V ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 )
18 r19.29r ⊢ ( ( ∃ 𝑦 ∈ V ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ V ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ V ( ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
19 r19.29 ⊢ ( ( ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
20 19 reximi ⊢ ( ∃ 𝑦 ∈ V ( ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
21 18 20 syl ⊢ ( ( ∃ 𝑦 ∈ V ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ V ∃ 𝑥 ∈ On 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
22 17 21 mpan2 ⊢ ( ∃ 𝑦 ∈ V ∀ 𝑥 ∈ On ¬ 𝑦 ∈ 𝐴 → ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
23 10 15 22 3syl ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
24 rexcom ⊢ ( ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ V ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
25 exancom ⊢ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
26 rexv ⊢ ( ∃ 𝑦 ∈ V ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
27 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ∧ ¬ 𝑦 ∈ 𝐴 ) )
28 25 26 27 3bitr4i ⊢ ( ∃ 𝑦 ∈ V ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )
29 28 rexbii ⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ V ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )
30 24 29 bitri ⊢ ( ∃ 𝑦 ∈ V ∃ 𝑥 ∈ On ( ¬ 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )
31 23 30 sylib ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )