Metamath Proof Explorer

Theorem bnj1452

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1452.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1452.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1452.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1452.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
bnj1452.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
bnj1452.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
bnj1452.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
bnj1452.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
bnj1452.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
bnj1452.10 ⊢ 𝑃 = ∪ 𝐻
bnj1452.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1452.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
bnj1452.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
bnj1452.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
Assertion bnj1452 ( 𝜒 → 𝐸 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1452.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1452.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1452.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1452.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1452.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1452.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
7 bnj1452.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1452.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1452.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1452.10 ⊢ 𝑃 = ∪ 𝐻
11 bnj1452.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12 bnj1452.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
13 bnj1452.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
14 bnj1452.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
15 5 7 bnj1212 ⊢ ( 𝜒 → 𝑥 ∈ 𝐴 )
16 15 snssd ⊢ ( 𝜒 → { 𝑥 } ⊆ 𝐴 )
17 bnj1147 ⊢ trCl ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐴
18 17 a1i ⊢ ( 𝜒 → trCl ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐴 )
19 16 18 unssd ⊢ ( 𝜒 → ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ⊆ 𝐴 )
20 14 19 eqsstrid ⊢ ( 𝜒 → 𝐸 ⊆ 𝐴 )
21 elsni ⊢ ( 𝑧 ∈ { 𝑥 } → 𝑧 = 𝑥 )
22 21 adantl ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ { 𝑥 } ) → 𝑧 = 𝑥 )
23 bnj602 ⊢ ( 𝑧 = 𝑥 → pred ( 𝑧 , 𝐴 , 𝑅 ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
24 22 23 syl ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ { 𝑥 } ) → pred ( 𝑧 , 𝐴 , 𝑅 ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
25 6 simplbi ⊢ ( 𝜓 → 𝑅 FrSe 𝐴 )
26 7 25 bnj835 ⊢ ( 𝜒 → 𝑅 FrSe 𝐴 )
27 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
28 26 15 27 syl2anc ⊢ ( 𝜒 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
29 28 ad2antrr ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ { 𝑥 } ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
30 24 29 eqsstrd ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ { 𝑥 } ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
31 ssun4 ⊢ ( pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
32 31 14 sseqtrrdi ⊢ ( pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 )
33 30 32 syl ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ { 𝑥 } ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 )
34 26 ad2antrr ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
35 simpr ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
36 17 35 bnj1213 ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ 𝐴 )
37 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
38 34 36 37 syl2anc ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑧 , 𝐴 , 𝑅 ) )
39 15 ad2antrr ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → 𝑥 ∈ 𝐴 )
40 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
41 34 39 35 40 syl3anc ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → trCl ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
42 38 41 sstrd ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
43 42 32 syl ⊢ ( ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) ∧ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 )
44 14 bnj1424 ⊢ ( 𝑧 ∈ 𝐸 → ( 𝑧 ∈ { 𝑥 } ∨ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
45 44 adantl ⊢ ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) → ( 𝑧 ∈ { 𝑥 } ∨ 𝑧 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
46 33 43 45 mpjaodan ⊢ ( ( 𝜒 ∧ 𝑧 ∈ 𝐸 ) → pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 )
47 46 ralrimiva ⊢ ( 𝜒 → ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 )
48 snex ⊢ { 𝑥 } ∈ V
49 48 a1i ⊢ ( 𝜒 → { 𝑥 } ∈ V )
50 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → trCl ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
51 26 15 50 syl2anc ⊢ ( 𝜒 → trCl ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
52 49 51 bnj1149 ⊢ ( 𝜒 → ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∈ V )
53 14 52 eqeltrid ⊢ ( 𝜒 → 𝐸 ∈ V )
54 1 bnj1454 ⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝐵 ↔ [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ) )
55 53 54 syl ⊢ ( 𝜒 → ( 𝐸 ∈ 𝐵 ↔ [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ) )
56 bnj602 ⊢ ( 𝑥 = 𝑧 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑧 , 𝐴 , 𝑅 ) )
57 56 sseq1d ⊢ ( 𝑥 = 𝑧 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ↔ pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
58 57 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ↔ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
59 58 anbi2i ⊢ ( ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ↔ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
60 59 sbcbii ⊢ ( [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ↔ [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
61 55 60 bitrdi ⊢ ( 𝜒 → ( 𝐸 ∈ 𝐵 ↔ [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ) )
62 sseq1 ⊢ ( 𝑑 = 𝐸 → ( 𝑑 ⊆ 𝐴 ↔ 𝐸 ⊆ 𝐴 ) )
63 sseq2 ⊢ ( 𝑑 = 𝐸 → ( pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ↔ pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) )
64 63 raleqbi1dv ⊢ ( 𝑑 = 𝐸 → ( ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ↔ ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) )
65 62 64 anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ↔ ( 𝐸 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) ) )
66 65 sbcieg ⊢ ( 𝐸 ∈ V → ( [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ↔ ( 𝐸 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) ) )
67 53 66 syl ⊢ ( 𝜒 → ( [ 𝐸 / 𝑑 ] ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑑 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) ↔ ( 𝐸 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) ) )
68 61 67 bitrd ⊢ ( 𝜒 → ( 𝐸 ∈ 𝐵 ↔ ( 𝐸 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐸 pred ( 𝑧 , 𝐴 , 𝑅 ) ⊆ 𝐸 ) ) )
69 20 47 68 mpbir2and ⊢ ( 𝜒 → 𝐸 ∈ 𝐵 )