Metamath Proof Explorer

Theorem inf3lem3

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg . (Contributed by NM, 29-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
inf3lem.3 ⊢ 𝐴 ∈ V
inf3lem.4 ⊢ 𝐵 ∈ V
Assertion inf3lem3 ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 ⊢ 𝐴 ∈ V
4 inf3lem.4 ⊢ 𝐵 ∈ V
5 1 2 3 4 inf3lemd ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 )
6 1 2 3 4 inf3lem2 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )
7 6 com12 ⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )
8 pssdifn0 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ⊆ 𝑥 ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) → ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ )
9 5 7 8 syl6an ⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ ) )
10 vex ⊢ 𝑥 ∈ V
11 10 difexi ⊢ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∈ V
12 zfreg ⊢ ( ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ ) → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
13 11 12 mpan ⊢ ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
14 eldifi ⊢ ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → 𝑣 ∈ 𝑥 )
15 inssdif0 ⊢ ( ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
16 15 biimpri ⊢ ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) )
17 14 16 anim12i ⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
18 vex ⊢ 𝑣 ∈ V
19 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
20 1 2 18 19 inf3lema ⊢ ( 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ ( 𝑣 ∈ 𝑥 ∧ ( 𝑣 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
21 17 20 sylibr ⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) )
22 1 2 3 4 inf3lemc ⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) )
23 22 eleq2d ⊢ ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ↔ 𝑣 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
24 21 23 imbitrrid ⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) )
25 eldifn ⊢ ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) )
27 24 26 jca2 ⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ) )
28 eleq2 ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ↔ 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) )
29 28 biimprd ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) )
30 iman ⊢ ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) ↔ ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) )
31 29 30 sylib ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) )
32 31 necon2ai ⊢ ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) )
33 27 32 syl6 ⊢ ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
34 33 expd ⊢ ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) )
35 34 rexlimdv ⊢ ( 𝐴 ∈ ω → ( ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ) = ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
36 13 35 syl5 ⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ∖ ( 𝐹 ‘ 𝐴 ) ) ≠ ∅ → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
37 9 36 syldc ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )