This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aomclem2

Description: Lemma for dfac11 . Successor case 2, a choice function for subsets of ( R1dom z ) . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses aomclem2.b ⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
aomclem2.c ⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
aomclem2.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
aomclem2.su ⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
aomclem2.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
aomclem2.a ⊢ ( 𝜑 → 𝐴 ∈ On )
aomclem2.za ⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
aomclem2.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion aomclem2 ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )

Proof

Step Hyp Ref Expression
1 aomclem2.b ⊢ 𝐵 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( ( 𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑧 ) ( 𝑑 ( 𝑧 ‘ ∪ dom 𝑧 ) 𝑐 → ( 𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏 ) ) ) }
2 aomclem2.c ⊢ 𝐶 = ( 𝑎 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
3 aomclem2.on ⊢ ( 𝜑 → dom 𝑧 ∈ On )
4 aomclem2.su ⊢ ( 𝜑 → dom 𝑧 = suc ∪ dom 𝑧 )
5 aomclem2.we ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑧 ( 𝑧 ‘ 𝑎 ) We ( 𝑅1 ‘ 𝑎 ) )
6 aomclem2.a ⊢ ( 𝜑 → 𝐴 ∈ On )
7 aomclem2.za ⊢ ( 𝜑 → dom 𝑧 ⊆ 𝐴 )
8 aomclem2.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
9 vex ⊢ 𝑎 ∈ V
10 3 6 jca ⊢ ( 𝜑 → ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) )
11 r1ord3 ⊢ ( ( dom 𝑧 ∈ On ∧ 𝐴 ∈ On ) → ( dom 𝑧 ⊆ 𝐴 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) ) )
12 10 7 11 sylc ⊢ ( 𝜑 → ( 𝑅1 ‘ dom 𝑧 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
13 12 sspwd ⊢ ( 𝜑 → 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝐴 ) )
14 13 sseld ⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ) )
15 rsp ⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) )
16 8 14 15 sylsyld ⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ) )
17 16 3imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) )
18 17 eldifad ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) )
19 inss1 ⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑎
20 19 sseli ⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ∈ 𝒫 𝑎 )
21 20 elpwid ⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 )
22 18 21 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ 𝑎 )
23 1 3 4 5 aomclem1 ⊢ ( 𝜑 → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )
24 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) )
25 inss2 ⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ Fin
26 25 18 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ∈ Fin )
27 eldifsni ⊢ ( ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ )
28 17 27 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ≠ ∅ )
29 elpwi ⊢ ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
30 29 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
31 22 30 sstrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) )
32 fisupcl ⊢ ( ( 𝐵 Or ( 𝑅1 ‘ dom 𝑧 ) ∧ ( ( 𝑦 ‘ 𝑎 ) ∈ Fin ∧ ( 𝑦 ‘ 𝑎 ) ≠ ∅ ∧ ( 𝑦 ‘ 𝑎 ) ⊆ ( 𝑅1 ‘ dom 𝑧 ) ) ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) )
33 24 26 28 31 32 syl13anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ ( 𝑦 ‘ 𝑎 ) )
34 22 33 sseldd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 )
35 2 fvmpt2 ⊢ ( ( 𝑎 ∈ V ∧ sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) ∈ 𝑎 ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
36 9 34 35 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) = sup ( ( 𝑦 ‘ 𝑎 ) , ( 𝑅1 ‘ dom 𝑧 ) , 𝐵 ) )
37 36 34 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 )
38 37 3exp ⊢ ( 𝜑 → ( 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) → ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) ) )
39 38 ralrimiv ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ dom 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶 ‘ 𝑎 ) ∈ 𝑎 ) )