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 sseldi ( ( 𝜑𝑎 ∈ 𝒫 ( 𝑅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 𝑧 ) ( 𝑎 ≠ ∅ → ( 𝐶𝑎 ) ∈ 𝑎 ) )